Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model

Kevin Kappelmann, Fabian Huch, Lukas Stevens, Mohammad Abdulaziz

TL;DR

The work tackles the challenge of formalising and verifying algorithms within a computation model that is both time- and space-efficient from a complexity-theoretic perspective. It introduces a semi-automated pipeline that starts from tail-recursive, first-order functions in a subset of Isabelle/HOL, translates them into a verified IMP-based language $ ext{$IMP^{ m TC}$}$, and then progressively compiles to a highly space-efficient final model $ ext{$IMP^{-}$}$ via a chain of verified steps, with linear blow-up at each stage. A key novelty is the certified synthesis and automated equivalence proofs between the HOL inputs and the generated imperative programs, enabling formal verification of complexity-theoretic properties for practical algorithms (e.g., maps, folds, bisection, and reductions). The framework lays groundwork for formalising major theorems in complexity theory (e.g., Cook-Levin) by providing a controlled, verifiable path from high-level functional specifications to bounded, bit-level computations.

Abstract

We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that can simulate (and be simulated by) Turing Machines with a quadratic time and constant space blow-up. Our framework derives while-programs from functional programs written in a subset of Isabelle/HOL, namely tail-recursive functions with first-order arguments and algebraic datatypes. As far as we are aware, it is the first framework targeting a computation model that is reasonable in time and space from a complexity-theoretic perspective.

Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model

TL;DR

The work tackles the challenge of formalising and verifying algorithms within a computation model that is both time- and space-efficient from a complexity-theoretic perspective. It introduces a semi-automated pipeline that starts from tail-recursive, first-order functions in a subset of Isabelle/HOL, translates them into a verified IMP-based language IMP^{ m TC}, and then progressively compiles to a highly space-efficient final model IMP^{-} via a chain of verified steps, with linear blow-up at each stage. A key novelty is the certified synthesis and automated equivalence proofs between the HOL inputs and the generated imperative programs, enabling formal verification of complexity-theoretic properties for practical algorithms (e.g., maps, folds, bisection, and reductions). The framework lays groundwork for formalising major theorems in complexity theory (e.g., Cook-Levin) by providing a controlled, verifiable path from high-level functional specifications to bounded, bit-level computations.

Abstract

We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that can simulate (and be simulated by) Turing Machines with a quadratic time and constant space blow-up. Our framework derives while-programs from functional programs written in a subset of Isabelle/HOL, namely tail-recursive functions with first-order arguments and algebraic datatypes. As far as we are aware, it is the first framework targeting a computation model that is reasonable in time and space from a complexity-theoretic perspective.

Paper Structure

This paper contains 7 sections, 1 theorem, 4 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Why?
  3. Contribution
  4. Availability
  5. Preliminaries
  6. $\mathrm{HOL}^{\mathrm{TC}\mathsf{\mathbb{N}}}$ to $\mathsf{IMP}^{\mathrm{TC}}$
  7. Note on Higher-Order Functions

Key Result

theorem thmcountertheorem

If $\text{max}\,\{s_{\text{max}},p_{\text{max}}\} < 2^w$ and $(p,s)\Rightarrow^{n}s'$, then $s'_{\text{max}} < 2^{w+n}$.

Figures (4)

  • Figure 1: Compilation pipeline from $\mathrm{HOL}^{\mathrm{TC}}$ functions to $\mathsf{IMP}^{\mathrm{-}}$ programs.
  • Figure 2: Grammar for body $t$ of a first-order function $f=\lambda\vv{x}.\, t$ with ADTs.
  • Figure 3: Semantics shared by our $\mathsf{IMP}$-languages, excluding the final $\mathsf{IMP}^{\mathrm{-}}$.
  • Figure 4: Execution relation of $\mathsf{IMP}^{\mathrm{TC}}$-specific commands.

Theorems & Definitions (2)

  • theorem thmcountertheorem
  • proof : Proof sketch