A logic for program extraction with bounded non-determinism

Ulrich Berger, Swansea University. Part of the algebra, logic and algorithms seminar series.

Joint work with Hideki Tsuiki, Kyoto University

Programs extracted from constructive proofs are usually deterministic. We introduce a constructive logic with two new logical operators that allow for the extraction of provably correct non-deterministic programs from proofs. The first is a unary operator S_n(A) that permits the realization of a formula A by choosing non-deterministically among n given candidate realizations of A. The second is a binary operation A|B (read "A restricted to B"), strengthening implication B -> A. Restriction is necessary to be able to infer formulas of the form S_n(A). Curiously, the main rule for introducing S_n(A) is a form of the law of excluded middle. So, one can say that the law of excluded middle is constructive, however in a non-deterministic way.

We apply the new system to the extraction of non-deterministic programs in computable analysis (translation of Hideki\'s infinite Gray code into signed digit representation [1]) and linear algebra (Gaussian elimination).

A preliminary version of part of this work was presented at CSL 2016 [2].

[1] Hideki Tsuiki. Real number computation through Gray code embedding. Theoretical Computer Science, 284:467--485, 2002.

[2] Ulrich Berger. Extracting Non-Deterministic Concurrent Programs. LIPIcs 62:26:1--26:21, 2016.

Ulrich Berger, Swansea University