# 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

#### Related events

See all Pure Mathematics events