Logic & Programming

I am giving a distilled tutorial during the conference PPDP 2014. The topic is writing proofs in continuation passing style, with the xase study of normalization-by-evaluation for Gödel's System T extended with delimited control. Tutorial web page is up.

https://iaddg.net/danko/PPDP-2014-tutorial/

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

My paper on type isomorphisms in the presence of sums was accepted to CSL-LICS 2014.

http://arxiv.org/abs/1401.2567

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

I will be serving on the program committee for the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP) taking place in Canterbury, UK on September 8-10, 2014

http://www.cs.kent.ac.uk/events/2014/ppdp-lopstr-14/

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

The paper “A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators”, coauthored with Keiko Nakata, accepted for publication

http://arxiv.org/abs/1209.2229

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

I will give a talk on type isomorphisms on the Deducteam seminar at INRIA Paris — av. de Italie, on February 7, 2014, at 10:00.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

I will give a talk at the seminar of the LCR team, Université Paris 13 (March 7).

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

I will give a talk at Kosta Došen's General Proof Theory seminar at the Serbian Academy of Sciences and Arts (February 24).

http://www.mi.sanu.ac.rs/seminars/seminar18.htm

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

I set up a web page with materials for the winter school Recent developments in Type Theory, Mathematical Structures of Computation – Lyon 2014.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

My PhD thesis has been approved for defense. You can find it here : http://tel.archives-ouvertes.fr/tel-00529021/en/

Chapter 1 gives a constructive version of a Henkin-style proof of Godel's completeness theorem. Chapter 2 introduces a notion of model similar to Kripke models using which one can give a normalization-by-evaluation style proof of completeness for classical logic. Chapter 3 does the same thing for intuitionistic logic (including disjunction and the existential). Finally, Chapter 4 presents an extension of intuitionistic logic with delimited control operators which still remains intuitionistic (preserves disjunction and existence properties) and can prove the Double Negation Shift and Markov's Principle.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

Published on Feb. 5th, 2010 on https://speleologic.livejournal.com/2595.html

The purpose of this post is a detailed proof, following Coquand[1], of the Open Induction Principle using Decidable-Bar Induction[2].

Open induction (OI) is useful when one can not do a proof by usual well-founded induction, that is, when there is no well-founded relation that can be used. In such cases, if the space one is in is compact, and the property one wants to prove is open, one can use a non-well-founded order to do an induction proof. From the computer science perspective, this means one can build a terminating recursive program for computing a property that does not depend on a structurally decreasing criterium of termination.

In this post we concentrate on Cantor space 2N, but it is, in some sense, enough, because every compact space is an image of Cantor space. A member α of 2N is a map N → 2, i.e. an infinite stream of bits, i.e. an infinite branch of the infinite binary tree. α<β if α is “left of” β as a branch of the infinite tree, that is, α<β if they are bit streams which are equal for a finite initial segment and then at some length n of the segment α(n) is “left” while β(n) is “right”. We write αn for the finite initial segment of α of lenght n. Each node in the infinite binary tree corresponds to some initial segment, and vice-versa. Each such node, i.e. each finite bit string, is called a basic open. An open, or open subspace, of Cantor space is an arbitrary union of basic opens. Equivalently, an open is determined by a Boolean function G on arbitrary lenght, but finite, bit strings, G : 2* → 2, which is monotone: If s, s′:2*, s is an initial segment of s′, and G(s)=⊤, then also G(s′)=⊤.

Axiom 1 (Decidable-Bar Induction) For all unary predicates P and Q on 2* (finite binary strings), such that P is decidable and ∀ s. P s → Q s, if ∀ α∈2N. ∃ n∈ N. P(αn) and ∀ s∈2*. (∀ b∈ 2. Q ⟨ b::s ⟩) → Q s then Q ⟨ ⟩.

Theorem 2 (Open Induction Principle) Let U be an open set of Cantor space 2N and < be a lexicographic ordering on 2N. If ∀ α. (∀ β<α. β∈ U) → α∈ U () then ∀ α. α∈ U. Proof. Let α : 2N be given. U is open in 2N, hence given by a mapping G : 2 → 2 which is monotone w.r.t. initial segments: if s is a prefix of t, G s = ⊤ implies G t = ⊤. We say that G bars s with witness k (notation G|k s) if all k−bit-extensions of s satisfy G.

We define mutually, by (primitive) recursion on finite strings of numbers, two functions f:N* → 2* and acc:N*→ 2:

acc ⟨ ⟩ = ⊤ acc ⟨ 0::s ⟩ = acc(s) acc ⟨ n+1::s ⟩ = acc(s) ∧ G|n ⟨ ⊥::f(s) ⟩

f ⟨ ⟩ = ⟨ ⟩ f ⟨ 0::s ⟩ = ⟨ ⊥::f(s) ⟩ f ⟨ n+1::s ⟩ = ⟨ acc⟨ n+1::s ⟩::f(s) ⟩ We set

P(s) := G(f(s)) Q(s) := acc(s) → ∃ m. G|m f(s) and apply bar induction, which gives us a proof of Q(⟨ ⟩), which, since acc(⟨ ⟩)=⊤, gives an m∈ N such that any bit-string with length m satisfies G. Hence, also αm, therefore α∈ U.

The hypotheses of (D-BI) are satisfied by the following lemmas.

Lemma 3 ∀ α∈NN. ∃ n∈ N. G(f(αn)) Proof. We write f(α) for the natural exension of f to infinite sequences. The lemma states that ∀ α∈NN. f(α)∈ U. Let α be given. Apply (). Let β<f(α), that is, there is some n such that βn = ⟨ ⊥::s ⟩ and ⟨ ⊤::s ⟩ = f(α) n = f(αn) for some s∈2 (of length n−1). By the defining equations of f and app, n>0, s=f(α(n−1)), acc(s) and G|k⟨ ⊥::s ⟩, that is, G|kβn, for some k. Hence, G(β(n+k)) = ⊤ i.e. β∈ U.

Lemma 4 For any s∈N*, if (∀ n∈ N. acc⟨ n::s ⟩ → ∃ m. G|m f⟨ n::s ⟩), and acc(s), then ∃ n. G|n f(s). Proof. Since acc(s), also acc⟨ 0::s ⟩, and the hypothesis gives us an m such that G|mf⟨ 0::s ⟩, that is, G|m⟨ ⊥::f(s) ⟩. This means that acc⟨ m+1::s ⟩, which we use with the hypothesis again to get a k such that G|kf⟨ m+1::s ⟩ i.e. Gk⟨ acc⟨ m+1::s ⟩::f(s) ⟩ i.e. G|k⟨ ⊤::f(s) ⟩. We showed that G bars both ⟨ ⊤::f(s) ⟩ and ⟨ ⊥::f(s) ⟩, which means that G bars f(s) already: G|max(m,k)f(s).

Lemma 5 ∀ s∈N*. G(f(s)) → acc(s) → ∃ m. G|m f(s). Proof. G(f(s)) iff G|0 f(s).

Remark 6 The given lemmas, and the functions f and acc, are more general than needed for (D-BI), since they take input of type N* instead of 2*.

References [1] Thierry Coquand. A note on the open induction principle, 1997. [2] Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics: An Introduction I and II, volume 121, 123 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1988.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net