Recurrence extraction and denotational semantics with recursive definitions

TL;DR

This paper presents a direct method for extracting recurrence relations from a language with general recursive functions and types, along with models for analyzing sorting algorithms, simplifying previous proofs.

Contribution

It introduces a new extraction function for recursive languages and provides simplified soundness proofs without logical relations.

Findings

Extraction function successfully models recursive functions and types.

Models for merge sort and quick sort validate the extracted recurrences.

Simplified proof technique enhances understanding of recurrence semantics.

Abstract

With one exception, our previous work on recurrence extraction and denotational semantics has focused on a source language that supports inductive types and structural recursion. The exception handles general recursion via an initial translation into call-by-push-value. In this note we give an extraction function from a language with general recursive function definitions and recursive types directly to a PCF-like recurrence language. We prove the main soundness result (that the syntactic recurrences in fact bound the operational cost) without the use of a logical relation, thereby significantly simplifying the proof compared to our previous work (at the cost of placing more demands on the models of the recurrence language). We then define two models of the recurrence language, one for analyzing merge sort, and another for analyzing quick sort, as case studies to understand model definitions for justifying the extracted recurrences.