Extracting total Amb programs from proofs

Hideki Tsuiki; Ulrich Berger

arxiv: 2307.12454 · v4 · submitted 2023-07-23 · 💻 cs.LO

Extracting total Amb programs from proofs

Ulrich Berger , Hideki Tsuiki This is my paper

Pith reviewed 2026-05-24 08:22 UTC · model grok-4.3

classification 💻 cs.LO

keywords program extractionnondeterminismconcurrencyintuitionistic logicamb operatordomain semanticscoinductionGray code

0 comments

The pith

CFP logic extracts total nondeterministic and concurrent programs from formal proofs by interpreting angelic choice.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents CFP, an intuitionistic first-order logic with inductive and coinductive definitions plus two new operators: Restriction, which strengthens implication, and a unary total-concurrency operator. From proofs in this system one extracts programs in a lambda calculus extended by the Amb constructor, interpreted operationally as globally angelic choice. Correctness and totality of the extracted programs are established by an intermediate domain-theoretic denotational semantics. The system thereby makes computationally usable certain variants of the law of excluded middle that appear in the rules for restriction and concurrency. The method is illustrated by extracting a program that converts infinite Gray code into signed-digit representation.

Core claim

CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by Restriction (binary) and a unary operator for total concurrency. Formal proofs in CFP yield lambda terms with the Amb constructor; these terms are provably total and correct with respect to the original specifications via a domain-theoretic semantics that models Amb as globally angelic choice.

What carries the argument

The Amb constructor for globally angelic choice, justified by the restriction and total-concurrency operators whose proof rules incorporate variants of excluded middle.

If this is right

Extracted programs are guaranteed total and correct with respect to their specifications.
Nondeterministic and concurrent behaviors become formally verifiable through proofs in CFP.
Proof rules involving classical principles become computationally realizable once Amb is available.
Concrete translations between infinite representations, such as Gray code to signed digits, can be realized by total nondeterministic programs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same technique might be applied to other choice primitives whose semantics can be captured domain-theoretically.
One could test whether the extracted Gray-code program indeed produces all possible signed-digit expansions on repeated runs.
CFP-style operators could be added to existing proof assistants to support verified extraction of programs with built-in nondeterminism.

Load-bearing premise

The domain-theoretic denotational semantics correctly models the operational behavior of Amb and ensures extracted programs satisfy the logical specifications.

What would settle it

An extracted Amb program obtained from a valid CFP proof that fails to terminate on some input or fails to satisfy the specification stated in the proof.

read the original abstract

We present a logical system CFP (Concurrent Fixed Point Logic) supporting the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators: Restriction (binary), a strengthening of implication, and a unary operator for total concurrency. The source of the extraction is formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy's amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of CFP is the fact that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb. This is a revised and extended version of the conference paper presented at ESOP 2022 with the same title that contains full proofs of all major results.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

CFP adds Restriction and total concurrency operators to extract total nondeterministic programs via Amb, with the full proofs now supplied.

read the letter

The main point is that this paper gives a concrete system CFP for pulling total, correct programs out of proofs even when nondeterminism and concurrency are involved. It adds two new operators—binary Restriction and unary total concurrency—whose rules rely on excluded-middle variants that only become usable because Amb supplies angelic choice. The target language is lambda calculus plus recursion and Amb; correctness goes through an intermediate domain-theoretic semantics, and they demonstrate it by extracting a translator from infinite Gray code to signed-digit form. This is the full version of the ESOP 2022 conference paper, now containing the extraction theorem and adequacy arguments in detail rather than sketches. The work sits on standard intuitionistic logic plus inductive and coinductive definitions, so the extension is localized and the extraction stays total. The modeling step that needs to hold is that the domain semantics matches the operational reading of Amb; the paper treats this as proven rather than assumed, which removes the main circularity risk. No internal contradictions appear in the setup or the example. Readers already working on program extraction from constructive proofs or on verified concurrent code will get direct use from the new operators and the worked example. Others outside that niche will see it as a solid but narrow advance. The presence of the full derivations makes the central claims checkable, so the paper is worth sending to referees even if they end up pressing on the adequacy details for Amb.

Referee Report

0 major / 3 minor

Summary. The paper introduces Concurrent Fixed Point Logic (CFP), an intuitionistic first-order logic extended with inductive and coinductive definitions, a binary Restriction operator (a strengthening of implication), and a unary total concurrency operator. Formal CFP proofs serve as the source for extracting programs in a lambda calculus extended by the Amb constructor (interpreted as globally angelic choice for nondeterminism and concurrency). Correctness and totality of extracted programs are established via an intermediate domain-theoretic denotational semantics that is shown adequate with respect to the operational semantics. The system is illustrated by extracting a nondeterministic program translating infinite Gray code into signed-digit representation. The proof rules for Restriction and concurrency incorporate variants of excluded middle that become computationally interpretable only in the presence of Amb. This is a revised and extended journal version of the ESOP 2022 conference paper, now containing full proofs of all major results including the extraction theorem.

Significance. If the central results hold, the work makes a substantive contribution to program extraction in the presence of nondeterminism and concurrency by providing a logically principled route to total, correct Amb programs. The explicit adequacy proof between domain-theoretic and operational semantics, together with the full formalization of the extraction theorem, supplies the kind of rigorous foundation that is often missing in extraction systems involving choice operators. The Gray-code example further demonstrates applicability to infinite data and coinductive reasoning.

minor comments (3)

[§1] §1 (Introduction): the precise syntactic distinction between the Restriction operator and ordinary implication is introduced only informally; an early displayed definition of the two connectives side-by-side would improve readability for readers unfamiliar with the ESOP version.
The domain-theoretic model is described as using 'standard' constructions, yet the precise choice of domain (e.g., whether it is the Plotkin powerdomain or a variant tailored to angelic choice) is not stated until the semantics section; an explicit sentence in the overview would help.
Table or figure numbering for the Gray-code extraction example is absent from the abstract and early sections; cross-references to the concrete extracted term and its specification would make the running example easier to track.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment and recommendation to accept. The summary accurately captures the core contributions of CFP, the extraction theorem, the adequacy result, and the Gray-code example.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper supplies explicit proofs of the extraction theorem and semantic adequacy for the Amb operator. These rest on standard intuitionistic logic with inductive/coinductive definitions plus domain theory, without any reduction of the main claims to fitted parameters, self-definitional equations, or load-bearing self-citations. The derivation chain is self-contained and externally verifiable via the stated proof rules and semantics.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 3 invented entities

The paper relies on standard background logic and domain theory while introducing new operators and the Amb entity; no free parameters are mentioned.

axioms (1)

standard math Intuitionistic first-order logic with inductive and coinductive definitions is sound and supports program extraction.
Core background for CFP as stated in the abstract.

invented entities (3)

Restriction operator no independent evidence
purpose: Binary strengthening of implication in CFP.
New operator introduced to support the extraction system.
Total concurrency operator no independent evidence
purpose: Unary operator for total concurrency in CFP.
New operator introduced to support the extraction system.
Amb constructor no independent evidence
purpose: Implements globally angelic choice for nondeterminism and concurrency in the target lambda calculus.
New constructor in the extraction target language.

pith-pipeline@v0.9.0 · 5721 in / 1320 out tokens · 44539 ms · 2026-05-24T08:22:12.011000+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators: Restriction (binary) ... and a unary operator for total concurrency.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.