Continuation-passing Style Models Complete for
Intuitionistic Logic

arXiv:1102.1061v2 [math.LO] 3 Mar 2011

Danko Ilik
University “Goce Delčev” – Štip
Address: Faculty of Informatics, PO Box 201, Štip, Macedonia
E-mail: dankoilik@gmail.com

Abstract
A class of models is presented, in the form of continuation monads polymorphic for
first-order individuals, that is sound and complete for minimal intuitionistic predicate
logic. The proofs of soundness and completeness are constructive and the computational content of their composition is, in particular, a β-normalisation-by-evaluation
program for simply typed lambda calculus with sum types. Although the inspiration
comes from Danvy’s type-directed partial evaluator for the same lambda calculus, the
there essential use of delimited control operators (i.e. computational effects) is avoided.
The role of polymorphism is crucial – dropping it allows one to obtain a notion of
model complete for classical predicate logic. The connection between ours and Kripke
models is made through a strengthening of the Double-negation Shift schema.
Key words: intuitionistic logic, completeness, Kripke models, Double-negation Shift,
normalization by evaluation
2000 MSC: 03B20, 03B35, 03B40, 68N18, 03F55, 03F50, 03B55

1. Introduction
Although Kripke models are standard semantics for intuitionistic logic, there is
as yet no (simple) constructive proof of their completeness when one considers all
logical connectives. While Kripke’s original proof [20] was classical, Veldman gave an
intuitionistic one [26] by using Brouwer’s Fan Theorem to handle disjunction and the
existential quantifier. To see what the computational content behind Veldman’s proof
is, one might consider a realisability interpretation of the Fan Theorem (for example
[3]), but, all known realisers being defined by general recursion, due to the absence of
an elementary proof of their termination, it is not clear whether one can think of the
program using them as a constructive proof or not.
On the other hand, a connection between normalisation-by-evaluation (NBE) [4]
for simply typed lambda calculus, λ→ , and completeness for Kripke models for the
fragment {∧, ⇒, ∀} has been made [6, 15]. We review this connection in Section 2.
There we also look at Danvy’s extension [8] of NBE from λ→ to λ→∨ , simply typed
lambda calculus with sum types. Even though Danvy’s algorithm is simple and elegant, he uses the full power of delimited control operators which do not yet have a
Preprint submitted to Elsevier

March 25, 2018

typing system that permits to understand them logically. We deal with that problem
in Section 3, by modifying the notion of Kripke model so that we can give a proof
of completeness for full intuitionistic logic in continuation-passing style, that is, without relying on having delimited control operators in our meta-language. In Section 4,
we extract the algorithm behind the given completeness proof, a β-NBE algorithm for
λ→∨ . In Section 5, we stress the importance of our models being dependently typed, by
comparing them to similar models that are complete for classical logic [18]. We there
also relate our and Kripke models by showing that the two are equivalent in presence
of a strengthening of the Double-negation Shift schema [24, 25]. We conclude with
Section 6 by mentioning related work.
The proofs of Section 3 have been formalised in the Coq proof assistant in [16],
which also represents an implementation of the NBE algorithm.
2. Normalisation-by-Evaluation as Completeness
In [4], Berger and Schwichtenberg presented a proof of normalisation of λ→ which
does not involve reasoning about the associated reduction relation. Instead, they interpret λ-terms in a domain, or ambient meta-language, using an evaluation function,
J−K : Λ → D,
and then they define an inverse to this function, which from the denotation in D directly
extracts a term in βη-long normal form. The inverse function ↓, called reification, is
defined by recursion on the type τ of the term, at the same time defining an auxiliary
function ↑, called reflection:
↓τ : D → Λ-nf
↓τ := a 7→ a
↓τ→σ := S 7→ λa. ↓σ (S · ↑τ a)

τ-atomic
a-fresh

↑τ : Λ-ne → D
↑τ := a 7→ a
↑τ→σ := e 7→ S 7→↑σ e(↓τ S )

τ-atomic

Here, S ranges over members of D, and we used 7→ and · for abstraction and application at the meta-level. The subclasses of normal and neutral λ-terms are given by the
following inductive definition.
Λ-nf ∋ r := λaτ .rσ | eτ
Λ-ne ∋ e := aτ | eτ→σ rτ

λ-terms in normal form
neutral λ-terms

It was a subsequent realisation of Catarina Coquand [6], that the evaluation algorithm J·K is also the one underlying the Soundness Theorem for minimal intuitionistic
logic (with ⇒ as the sole logical connective) with respect to Kripke models, and that
the reification algorithm ↓ is also the one underlying the corresponding Completeness
Theorem.
2

Definition 2.1. A Kripke model is given by a preorder (K, ≤) of possible worlds, a
binary relation of forcing (−) (−) between worlds and atomic formulae, and a family
of domains of quantification D(−), such that,
for all w′ ≥ w, w X → w′ X, and
for all w′ ≥ w, D(w) ⊆ D(w′ ).
The relation of forcing is then extended from atomic to composite formulae by the
clauses:
w

A ∧ B := w

A and w

B

w A ∨ B := w A or w B
w A ⇒ B := for all w′ ≥ w, w′

A ⇒ w′

′

′

B
′

w

∀x.A(x) := for all w ≥ w and t ∈ D(w ), w

w

∃x.A(x) := for some t ∈ D(w), w
w ⊥ := false
w

A(t)

A(t)

⊤ := true

More precisely, the following well-known statements hold and their proofs have
been machine-checked [7, 15] for the logic fragment generated by the connectives {⇒
, ∧, ∀}.
Theorem 2.2 (Soundness). If Γ ⊢ p : A then, in any Kripke model, for any world w, if
w Γ then w A.
Proof. By a simple induction on the length of the derivation.
Theorem 2.3 (Model Existence or Universal Completeness). There is a model U (the
“universal model”) such that, given a world w of U, if w A, then there exists a term
p and a derivation in normal form w ⊢ p : A.
Proof. The universal model U is built by setting:
• K to be the set of contexts Γ;
• “≤” to be the subset relation of contexts;
• “Γ
X” to be the set of derivations in normal form Γ ⊢nf X, for X an atomic
formula.
One then proves simultaneously, by induction on the complexity of A, that the two
functions defined above, reify (↓) and reflect (↑), are correct, that is, that ↓ maps a
member of Γ
A to a normal proof term (derivation) Γ ⊢ p : A, and that ↑ maps a
neutral term (derivation) Γ ⊢ e : A to a member of Γ A.
Corollary 2.4 (Completeness (usual formulation)). If in any Kripke model, at any
world w, w Γ implies w A, then there exists a term p and a derivation Γ ⊢ p : A.

3

Proof. If w
Γ→w
A in any Kripke model, then also w
Γ→w
A in the
model U above. Since from the ↑-part of Theorem 2.3 we have that Γ Γ, then from
the ↓-part of the same theorem there exists a term p such that Γ ⊢ p : A.
If one wants to extend this technique for proving completeness for Kripke models to
the rest of the intuitionistic connectives, ⊥, ∨ and ∃, the following meta-mathematical
problems appear, which have been investigated in the middle of the last century. At
that time, Kreisel, based on observations of Gödel, showed (Theorem 1 of [19]) that
for a wide range of intuitionistic semantics, into which Kripke’s can also be fit:
• If one can prove the completeness for the negative fragment of formulae (built
using ∧, ⊥, ⇒, ∀, and negated atomic formulae, X ⇒ ⊥) then one can prove
Markov’s Principle. In view of Theorem 2.3, this implies that having a completeness proof cover ⊥ means being able to prove Markov’s Principle – which
is known to be independent of many constructive logical systems, like Heyting
Arithmetic or Constructive Type Theory.
• If one can prove the completeness for all connectives, i.e. including ∨ and ∃,
then one can prove a strengthening1 of the Double-negation Shift schema on
Σ01 -formulae, which is also independent because it implies Markov’s Principle.
We mentioned that Veldman [26] used Brouwer’s Fan Theorem to handle ∨ and ∃,
but to handle ⊥ he included in his version of Kripke models an “exploding node”
predicate, ⊥ and defined w
⊥ := w ⊥ . We remark in passing that Veldman’s
modification does not defy Kripke original definition, but only makes it more regular:
if in Definition 2.1 one considers ⊥ as an atomic formula, rather than a composite one,
one falls back to Veldman’s definition.
One can also try to straightforwardly extend the NBE-Completeness proof to cover
disjunction (the existential quantifier is analogous) and see what happens. If one does
that, one sees that a problem appears in the case of reflection of sum, ↑A∨B . There,
given a neutral λ-term that derives A ∨ B, one is supposed to prove that w
A∨B
holds, which by definition means to prove that either w
A or w
B holds. But,
since the input λ-term is neutral, it represents a blocked computation from which we
will only be able to see whether A or B was derived, once we substitute values for the
contained free variables that block the computation.
That is where the solution of Olivier Danvy appears. In [8], he used the full power2
of the delimited control operators shift (Sk.p) and reset (#) [10] to give the following
1A

special case of D-DNS+ from page 13.
We say “full power” because his usage of delimited control operators is strictly more powerful than what
is possible with (non-delimited) control operators like call/cc. Danvy’s program makes non-tail calls with
continuations, while in the CPS translation of a program that uses call/cc all continuation calls are tail calls.
2

4

normalisation-by-evaluation algorithm for λ→∨ :
↓τ : D → Λ-nf
↓τ := a 7→ a
τ→σ

↓

↓τ∨σ

τ-atomic
σ

τ

:= S 7→ λa.# ↓ (S · ↑ a)
(
ι1 (↓τ S ′ ) , if S = inl ·S ′
:= S 7→
ι2 (↓σ S ′ ) , if S = inr ·S ′

↑τ : Λ-ne → D
↑τ := a 7→ a
τ→σ

a-fresh

τ-atomic
σ

τ

↑
:= e 7→ S 7→↑ e(↓ S )
↑τ∨σ := e 7→ Sκ.case e of (a1 .#κ · (inl ·(↑τ a1 ))ka2 .#κ · (inr ·(↑σ a2 )))

ai -fresh

We characterise explicitly normal and neutral λ-terms by the following inductive definitions.
Λ-nf ∋ r := eτ | λaτ .rσ | ιτ1 r | ιτ2 r


Λ-ne ∋ e := aτ | eτ→σ rτ | case eτ∨σ of aτ1 .r1ρ kaσ2 .r2ρ
Given Danvy’s NBE algorithm, which is simple and appears correct3, does this
mean that we can obtain a constructive proof of completeness for Kripke models if
we permit delimited control operators in our ambient meta-language? Unfortunately,
not, or not yet, because the available typing systems for them are either too complex
(type-and-effect systems [10] change the meaning of implication), or do not permit to
type-check the algorithm as a completeness proof (for example the typing system from
[12], or the one from Chapter 4 of [17]).
3. Kripke-CPS Models and Their Completeness
However, there is a close connection between shift and reset, and the continuationpassing style (CPS) translations [11]. We can thus hope to give a normalisation-byevaluation proof for full intuitionistic logic in continuation-passing style.
In this section we present a notion of model that we developed following this idea,
by suitably inserting continuations into the notion of Kripke model. We prove that the
new models are sound and complete for full intuitionistic predicate logic.
Definition 3.1. An Intuitionistic Kripke-CPS model (IK-CPS) is given by:
• a preorder (K, ≤) of possible worlds;
• a binary relation on worlds (−)

(−)
⊥

labelling a world as exploding;

3 For more details on the computational behaviour of shift/reset and the algorithm itself, we refer the
reader to the original paper [8] and to Section 3.2 of [17].

5

• a binary relation (−)
lae, such that

s

(−) of strong forcing between worlds and atomic formufor all w′ ≥ w, w

s

X → w′

s

X,

• and a domain of quantification D(w) for each world w, such that
for all w′ ≥ w, D(w) ⊆ D(w′ ).
The relation (−) s (−) of strong forcing is extended from atomic to composite formulae
inductively and by simultaneously defining one new relation, (non-strong) forcing:
A) if, for any formula C,

⋆ A formula A is forced in the world w (notation w

∀w′ ≥ w. ∀w′′ ≥ w′ . w′′

s

A → w′′

• w

s

A ∧ B if w

A and w

• w

s

A ∨ B if w

A or w

• w

s

A ⇒ B if for all w′ ≥ w, w

• w

s

∀x.A(x) if for all w′ ≥ w and all t ∈ D(w′ ), w′

• w

s

∃x.A(x) if w

C
⊥



→ w′

C
⊥;

B;
B;
A implies w

B;
A(t);

A(t) for some t ∈ D(w).

Remark 3.2. Certain details of the definition have been put into boxes to facilitate the
comparison carried out in Section 5.
Lemma 3.3. Strong forcing and (non-strong) forcing are monotone in any IK-CPS
model, that is, given w′ ≥ w, w s A implies w′ s A, and w A implies w′ A.
Proof. Monotonicity of strong forcing is proved by induction on the complexity of the
formula, while that of forcing is by definition. The proof is easy and available in the
Coq formalisation.
Lemma 3.4. The following monadic operations are definable for IK-CPS models:
“unit” η(·) w

s

A→w

A

“bind” (·)∗ (·) (∀w′ ≥ w. w′

s

A → w′

B) → w

A→w

B

Proof. Easy, using Lemma 3.3. If we leave implicit the handling of formulae C,
worlds, and monotonicity, we have the following procedures behind the proofs.
η(α) = κ 7→ κ · α
(φ)∗ (α) = κ 7→ α · (β 7→ φ · β · κ)

6

(a : A) ∈ Γ
Ax
Γ⊢a:A
Γ ⊢ p : A1
Γ ⊢ q : A2
∧I
Γ ⊢ (p, q) : A1 ∧ A2

Γ ⊢ p : A1 ∧ A2 i
∧E
Γ ⊢ π i p : Ai

Γ ⊢ p : Ai
∨i
Γ ⊢ ι i p : A1 ∨ A2 I
Γ ⊢ p : A1 ∨ A2

Γ, a1 : A1 ⊢ q1 : C
Γ, a2 : A2 ⊢ q2 : C
∨E
Γ ⊢ case p of (a1 .q1 ka2 .q2 ) : C

Γ, a : A1 ⊢ p : A2
⇒I
Γ ⊢ λa.p : A1 ⇒ A2

Γ ⊢ p : A1 ⇒ A2
Γ ⊢ q : A1
⇒E
Γ ⊢ pq : A2

Γ ⊢ p : A(x)
x-fresh
∀I
Γ ⊢ λx.p : ∀x.A(x)

Γ ⊢ p : ∀x.A(x)
∀E
Γ ⊢ pt : A(t)

Γ ⊢ p : A(t)
∃I
Γ ⊢ (t, p) : ∃x.A(x)
Γ ⊢ p : ∃x.A(x)
Γ, a : A(x) ⊢ q : C
Γ ⊢ dest p as (x.a) in q : C

x-fresh

∃E

Table 1: Proof term annotation for the natural deduction system of minimal intuitionistic predicate logic (MQC)
With Table 1, we fix a derivation system and proof term notation for minimal intuitionistic predicate logic. There are two kinds of variables, proof term variables a, b, . . .
and individual (quantifier) variables x, y, . . .. Individual constants are denoted by t. We
rely on these conventions to resolve the apparent ambiguity of the syntax: the abstraction λa.p is a proof term for implication, while λx.p is a proof term for ∀; (p, q) is a
proof term for ∧, while (t, q) is a proof term for ∃.
We supplement the characterisation of normal and neutral terms from page 5:
Λ-nf ∋ r :=e | λa.r | ι1 r | ι2 r | (r1 , r2 ) | λx.r | (t, r)
Λ-ne ∋ e :=a | er | case e of (a1 .r1 ka2 .r2 ) | π1 e | π2 e | et |
dest e as (x.a) in r
7

As before, let w

Γ denote that all formulae from Γ are forced.

Theorem 3.5 (Soundness). If Γ ⊢ p : A, then, in any world w of any IK-CPS model, if
w Γ, then w A.
Proof. This is proved by a simple induction on the length of the derivation. We give
the algorithm behind it in section 4.
Remark 3.6. The condition “for all formula C” in Definition 3.1 is only necessary for
the soundness proof to go through, more precisely, the cases of elimination rules for ∨
and ⇒. The completeness proof goes through even if we define forcing by


∀w′ ≥ w. ∀w′′ ≥ w′ . w′′ s A → w′′ ⊥A → w′ ⊥A .
Definition 3.7. The Universal IK-CPS model U is obtained by setting:
• K to be the set of contexts Γ of MQC;
• Γ ≤ Γ′ iff Γ ⊆ Γ′ ;
• Γ s X iff there is a derivation in normal form of Γ ⊢ X in MQC, where X is an
atomic formula;
• Γ

C
⊥

iff there is a derivation in normal form of Γ ⊢ C in MQC;

• for any w, D(w) is a set of individuals for MQC (that is, D(−) is a constant
function from worlds to sets of individuals).
(−)

s

(−) is monotone because of the weakening property for intuitionistic “⊢”.

Remark 3.8. The difference between strong forcing “ s ” and the exploding node predicate “ C⊥ ” in U is that the former is defined on atomic formulae, while the latter is
defined on any kind of formulae.
Lemma 3.9. We can also define the monadic “run” operation on the universal model
U, for atomic formulae X:
µ(·) : w

X→w

s

X.

Proof. By setting C := A and applying the identity function.
Theorem 3.10 (Completeness for U). For any closed formula A and closed context Γ,
the following hold for U:
Γ

A −→ {p | Γ ⊢ p : A}

Γ ⊢ e : A −→ Γ

A

(“reify”)

(↓)

(“reflect”)

(↑)

Moreover, the target of (↓) is a normal term, while the source of (↑) is a neutral term.

8

Proof. We prove simultaneously the two statements by induction on the complexity of
formula A.
We skip writing the proof term annotations, and write just Γ ⊢ A instead of “there
exists p such that Γ ⊢ p : A”, in order to decrease the level of detail. The algorithm
behind this proof that concentrates on proof terms is given in Section 4.
Base case. (↓) is by “run” (Lemma 3.9), (↑) is by “unit” (Lemma 3.4).
Induction case for ∧. Let Γ A ∧ B i.e.


∀C. ∀Γ′ ≥ Γ. ∀Γ′′ ≥ Γ′ . Γ′′ A and Γ′′ B → Γ′′ ⊢ C → Γ′ ⊢ C .

We apply this hypothesis by setting C := A ∧ B and Γ′ := Γ, and then, given Γ′′ ≥ Γ s.t.
Γ′′ A and Γ′′ B, we have to derive Γ′′ ⊢ A ∧ B. But, this is immediate by applying
the ∧I rule and the induction hypothesis (↓) twice, for A and for B.
Let Γ ⊢ A∧ B be a neutral derivation. We prove Γ A∧ B by applying unit (Lemma
3.4), and then applying the induction hypothesis (↓) on ∧1I , ∧2I , and the hypothesis.
Induction case for ∨. Let Γ A ∨ B i.e.


∀C. ∀Γ′ ≥ Γ. ∀Γ′′ ≥ Γ′ . Γ′′ A or Γ′′ B → Γ′′ ⊢ C → Γ′ ⊢ C .

We apply this hypothesis by setting C := A ∨ B and Γ′ := Γ, and then, given Γ′′ ≥ Γ
s.t. Γ′′ A or Γ′′
B, we have to derive Γ′′ ⊢ A ∨ B. But, this is immediate, after a
case distinction, by applying the ∨iI rule and the induction hypothesis (↓).
We now consider the only case (besides ↑∃xA(x) below) where using shift and reset,
or our Kripke-style models, is crucial. Let Γ ⊢ A ∨ B be a neutral derivation. Let a
formula C and Γ′ ≥ Γ be given, and let

∀Γ′′ ≥ Γ′ . Γ′′ A or Γ′′ B → Γ′′ ⊢ C .
(#)
We prove Γ′ ⊢ C by the following derivation tree:

A ∈ A, Γ′
Ax
A, Γ′ ⊢ A
(↑)
A, Γ′ A
inl
A, Γ′ A or A, Γ′ B
Γ⊢ A∨B
(#)
A, Γ′ ⊢ C
Γ′ ⊢ A ∨ B
Γ′ ⊢ C
Induction case for ⇒. Let Γ A ⇒ B i.e.
∀C. ∀Γ′ ≥ Γ.

∀Γ′′ ≥ Γ′ . ∀Γ3 ≥ Γ′′ . Γ3

A → Γ3

B ∈ B, Γ′
Ax
B, Γ′ ⊢ B
(↑)
B, Γ′ B
inr
B, Γ′ A or B, Γ′ B
(#)
B, Γ′ ⊢ C
∨E




B → Γ′′ ⊢ C → Γ′ ⊢ C .

We apply this hypothesis by setting C := A ⇒ B and Γ′ := Γ, and then, given Γ′′ ≥ Γ
s.t.
∀Γ3 ≥ Γ′′ . Γ3 A → Γ3 B
(#)
we have to derive Γ′′ ⊢ A ⇒ B. This follows by applying (⇒I ), the IH for(↓), then (#),
and finally the IH for (↑) with the Ax rule.
Let Γ ⊢ A ⇒ B be a neutral derivation. We prove Γ
A ⇒ B by applying unit
(Lemma 3.4), and then, given Γ′ ≥ Γ and Γ′ A, we have to show that Γ′ B. This is
done by applying the IH for (↑) on the (⇒E ) rule, with the IH for (↓) applied to Γ′ A.
9

Induction case for ∀. We recall that the domain function D(−) is constant in the
universal model U. Let Γ ∀xA(x) i.e.
∀C. ∀Γ′ ≥ Γ.

∀Γ′′ ≥ Γ′ . ∀Γ3 ≥ Γ′′ . ∀t ∈ D. Γ3




A(t) → Γ′′ ⊢ C → Γ′ ⊢ C .

We apply this hypothesis by setting C := ∀xA(x) and Γ′ := Γ, and then, given Γ′′ ≥ Γ
s.t.
∀Γ3 ≥ Γ′′ . ∀t ∈ D. Γ3 A(t)
(#)
we have to derive Γ′′ ⊢ ∀xA(x). This follows by applying (∀I ), the IH for(↓), and then
(#).
Let Γ ⊢ ∀xA(x) be a neutral derivation. We prove Γ
∀xA(x) by applying unit
(Lemma 3.4), and then, given Γ′ ≥ Γ and t ∈ D, we have to show that Γ′ A(t). This
is done by applying the IH for (↑) on the (∀E ) rule and the hypothesis Γ ⊢ ∀xA(x).
Induction case for ∃. Let Γ ∃xA(x) i.e.
∀C. ∀Γ′ ≥ Γ.

∀Γ′′ ≥ Γ′ . ∃t ∈ D. Γ′′




A(t) → Γ′′ ⊢ C → Γ′ ⊢ C .

We apply this hypothesis by setting C := ∃xA(x) and Γ′ := Γ, and then, given Γ′′ ≥ Γ
s.t. ∃t ∈ D. Γ′′ A(t), we have to derive Γ′′ ⊢ ∃xA(x). This follows by applying (∃I )
with t ∈ D, and the IH for(↓).
Let Γ ⊢ ∃xA(x) be a neutral derivation. Let a formula C and Γ′ ≥ Γ be given, and
let

∀Γ′′ ≥ Γ′ . ∃t ∈ D.Γ′′ A(t) → Γ′′ ⊢ C .
(#)

We prove Γ′ ⊢ C by the following derivation tree:

A(x) ∈ A(x), Γ′
Ax
A(x), Γ′ ⊢ A(x)
(↑)
′
Γ ⊢ ∃xA(x)
A(x), Γ
A(x)
(#)
Γ′ ⊢ ∃xA(x)
A(x), Γ′ ⊢ C
x-fresh
∃E
Γ′ ⊢ C
The result of reification “↓” is in normal form. By inspection of the proof.
4. Normalisation by Evaluation in IK-CPS Models
In this section we give the algorithm that we manually extracted from the Coq
formalisation, for the restriction to the interesting propositional fragment that involves
implication and disjunction. The algorithm extracted automatically by Coq contains
too many details to be instructive.

10

The following evaluation function for λ→∨ -terms is behind the proof of Theorem 3.5:
JΓ ⊢ p : AKw

Γ

:w

A

JaKρ := ρ(a)




Jλa.pKρ := κ 7→ κ · α 7→ JpKρ,a7→α = η · α 7→ JpKρ,a7→α


JpqKρ := κ 7→ JpKρ · φ 7→ φ · JqKρ · κ




Jι1 pKρ := κ 7→ κ · inl ·JpKρ = η · inl ·JpKρ




Jι2 pKρ := κ 7→ κ · inr ·JpKρ = η · inr ·JpKρ
(
!
Jq1 Kρ,a1 7→α · κ if γ = inl ·α
Jcase p of (a1 .q1 ka2 .q2 )Kρ := κ 7→ JpKρ · γ 7→
Jq2 Kρ,a2 7→β · κ if γ = inr ·β
The following is the algorithm behind Theorem 3.10:
↓ΓA : Γ
↑ΓA

A → {p ∈ Λ-nf | Γ ⊢ p : A}

: {e ∈ Λ-ne | Γ ⊢ e : A} → Γ

A

↓ΓX := α 7→ µ · α
↑ΓX
↓ΓA⇒B
↑ΓA⇒B
↓ΓA∨B
↑ΓA∨B

X-atomic

:= e 7→ η · e



B
A
:= η · φ 7→ λa. ↓Γ,a:A
φ· ↑Γ,a:A
a

 

:= e 7→ η · α 7→↑ΓB e ↓ΓA α
(
!
ι1 ↓ΓA α if γ = inl ·α
:= η · γ 7→
ι2 ↓ΓB β if γ = inr ·β





B
A
a2
:= e 7→ κ 7→ case e of a1 .κ · inl · ↑Γ,a
a1 ka2 .κ · inr · ↑Γ,a
2 :B
1 :A

X-atomic
a-fresh

ai -fresh

5. Variants and Relation to Kripke Models
5.1. “Call-by-value” Models
Defining forcing on composite formulae in Definition 3.1 proceeds analogously
to defining the call-by-name CPS translation [23], or Kolmogorov’s double-negation
translation [25, 22]. A definition analogous to the “call-by-value” CPS translation [23]
is also possible, by defining (non-strong) forcing by:
• w

s

A ∧ B if w

s

A and w

• w

s

A ∨ B if w

s

A or w

• w

s

A ⇒ B if for all w′ ≥ w, w

• w

s

∀x.A(x) if for all w′ ≥ w and all t ∈ D(w′ ), w′

s
s

B;

B;
s

A implies w

11

B;
A(t);

• w

s

∃x.A(x) if w

s

A(t) for some t ∈ D(w).

One can prove this variant of IK-CPS models sound and complete, similarly to
Section 3, except for two differences. Firstly, in the statement of Soundness, one needs
to put w s Γ in place of w Γ. Secondly, due to the first difference, the composition
of soundness of completeness that gives normalisation works for closed terms only.
5.2. Classical Models
In [16, 17, 18], we presented the following notion of model which is complete for
classical predicate logic and represents an NBE algorithm for it.
Definition 5.1. A Classical Kripke-CPS model (CK-CPS), is given by:
• a preorder (K, ≤) of possible worlds;
• a unary relation on worlds (−)
• a binary relation (−)
lae, such that

s

⊥

labelling a world as exploding;

(−) of strong forcing between worlds and atomic formufor all w′ ≥ w, w

s

X → w′

s

X,

• and a domain of quantification D(w) for each world w, such that
for all w′ ≥ w, D(w) ⊆ D(w′ ).
The relation (−) s (−) of strong forcing is extended from atomic to composite formulae
inductively and by simultaneously defining two new relations, refutation and (nonstrong) forcing:
⋆ A formula A is refuted in the world w (notation w : A
which strongly forces A, is exploding;
⋆ A formula A is forced in the world w (notation w
which refutes A, is exploding;
• w

s

A ∧ B if w

A and w

• w

s

A ∨ B if w

A or w

• w

s

A ⇒ B if for all w′ ≥ w, w

• w

s

∀x.A(x) if for all w′ ≥ w and all t ∈ D(w′ ), w′

• w

s

∃x.A(x) if w

) if any world w′ ≥ w,
A) if any world w′ ≥ w,

B;
B;
A implies w

B;
A(t);

A(t) for some t ∈ D(w).

The differences between Definition 3.1 and Definition 5.1 are marked with boxes.
We can also present CK-CPS using binary exploding nodes, by defining w s ⊥ :=
∀C.w C⊥ . Then, we get the following statement of forcing in CK-CPS,


∀w′ ≥ w. ∀w′′ ≥ w′ . w′′ s A → ∀I.w′′ ⊥I → ∀O.w′ O
⊥,
12

versus forcing in IK-CPS,

∀C. ∀w′ ≥ w. ∀w′′ ≥ w′ . w′′

s

A → w′′

C
⊥



→ w′

C
⊥

.

The difference between forcing in the intuitionistic and classical models is, then,
that: 1) the dependency on C is necessary in the intuitionistic case, while it is optional
in the classical case; 2) the continuation (the internal implication) in classical forcing is allowed to change the parameter C upon application, whereas in intuitionistic
forcing the parameter is not local to the continuation, but to the continuation of the
continuation.
At this point we also remark that the use of dependent types to handle the parameter
C is determined by the fact that we formalise our definitions in Intuitionistic Type Theory. Otherwise, the quantification ∀C. · · · is quantification over first-order individuals,
for example natural numbers.
5.3. Kripke Models
Let A(n) be an arbitrary first-order formula and let X(n, m) be a Σ01 -formula. Denote
the following arithmetic schema by (D-DNS+ ) for “dependent Double-negation Shift
schema, strengthened”.
∀m. ∀n1 ≥ n. (∀n2 ≥ n1 . A(n2 ) → X(n2, m)) → X(n1 , m)
D-DNS+
A(n)
Proposition 5.2. Let K = (K, ≤, D, , ⊥) be any structure such that  denotes forcing
in the standard Kripke model arising from K, and denotes (non-strong) forcing in
the IK-CPS model arising from the same K.
Then, in the presence of (D-DNS+ ) at meta-level, for all formula A, and any w ∈ K,
w  A ←→ w

A.

Proof. The proof is by induction on A, using (D-DNS+ ) to prove,


∀C. ∀w1 ≥ w. ∀w2 ≥ w1 . (w2 A or w2 B) → w2 C⊥ ) → w1

C
⊥

,

w A or w B
needed in the case for disjunction, and similarly for the existential quantifier.
Corollary 5.3. Completeness of full intuitionistic predicate logic with respect to standard Kripke models is provable constructively, in the presence of D-DNS+ .
Remark 5.4. It is the other direction of this implication that Kreisel proved, for a specialisation of D-DNS+ . (Section 2) To investigate more precisely whether D-DNS+
captures exactly constructive provability of completeness for Kripke models remains
future work.

13

6. Conclusion
We emphasised that our algorithm is β-NBE, because were we able to identify βηequal terms of λ→∨ through our NBE function, we would have solved the problem of
the existence of canonical η-long normal form for λ→∨ . However, as shown by [14],
due to the connection with Tarski’s High School Algebra Problem [5, 27], the notion
of such a normal form is not finitely axiomatisable. If one looks at examples of λ→∨ terms which are βη-equal but are not normalised to the same term by Danvy’s (and
our) algorithm, one can see that in the Coq type theory these terms are interpreted as
denotations that involve commutative cuts.
In recent unpublished work [9], Danvy also developed a version of his NBE algorithm directly in CPS, without using delimited control operators.
In [2], Barral gives a program for NBE of λ-calculus with sums by just using the
exceptions mechanism of a programming language, which is something a priori strictly
weaker than using delimited control operators.
In [1], Altenkirch, Dybjer, Hofmann, and Scott, give a topos theoretic proof of
NBE for a typed λ-calculus with sums, by constructing a sheaf model. The connection
between sheaves and Beth semantics4 is well known. While the proof is constructive,
due to their use of topos theory, we were unable to extract an algorithm from it.
In [21], Macedonio and Sambin present a notion of model for extensions of Basic
logic (a sub-structural logic more primitive than Linear logic), which, for intuitionistic
logic, appears to be related to our notion of model. However, they demand that their
set of worlds K be saturated, while we do not, and we can hence also work with finite
models.
In [13], Filinski proves the correctness of an NBE algorithm for Moggi’s computational λ-calculus, including sums. We found out about Filinski’s paper right before
finishing our own. He also evaluates the input terms in a domain based on continuations.
Acknowledgements
To Hugo Herbelin for inspiring discussions and, in particular, for suggesting to try
polymorphism, viz. Remark 3.6. To Olivier Danvy for suggesting reference [13].
References
[1] Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In LICS, pages
303–310, 2001.
[2] Freiric Barral. Exceptional NbE for sums. In Olivier Danvy, editor, Informal
proceedings of the 2009 Workshop on Normalization by Evaluation, August 15th
2009, Los Angeles, California, pages 21–30, 2009.
4 We remark that, for the fragment {⇒, ∀, ∧}, NBE can also be seen as completeness for Beth semantics,
since forcing in Beth and Kripke models is the same thing on that fragment.

14

[3] U. Berger and P. Oliva. Modified bar recursion and classical dependent choice.
In M. Baaz, S.D. Friedman, and J. Kraijcek, editors, Logic Colloquium ’01, Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Vienna, Austria, August 6 - 11, 2001, volume 20 of Lecture
Notes in Logic, pages 89–107. Springer, 2005.
[4] Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed lambda-calculus. In LICS, pages 203–211. IEEE Computer Society, 1991.
[5] Stanley Burris and Simon Lee. Tarski’s high school identities. The American
Mathematical Monthly, 100(3):231–236, 1993.
[6] Catarina Coquand. From semantics to rules: A machine assisted analysis. In CSL
’93, volume 832 of Lecture Notes in Computer Science, pages 91–105. Springer,
1993.
[7] Catarina Coquand. A formalised proof of the soundness and completeness of a
simply typed lambda-calculus with explicit substitutions. Higher Order Symbol.
Comput., 15(1):57–90, 2002.
[8] Olivier Danvy. Type-directed partial evaluation. In POPL, pages 242–257, 1996.
[9] Olivier Danvy. A call-by-name normalization function for the simply typed
lambda-calculus with sums and products. manuscript, 2008.
[10] Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical report, Computer Science Department, University of Copenhagen, 1989. DIKU Rapport 89/12.
[11] Olivier Danvy and Andrzej Filinski. Abstracting control. In LISP and Functional
Programming, pages 151–160, 1990.
[12] Andrzej Filinski. Controlling Effects. PhD thesis, School of Computer Science,
Carnegie Mellon University, 1996. Technical Report CMU-CS-96-119 (144pp.).
[13] Andrzej Filinski. Normalization by evaluation for the computational lambdacalculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications,
volume 2044 of Lecture Notes in Computer Science, pages 151–165. Springer
Berlin / Heidelberg, 2001.
[14] Marcelo P. Fiore, Roberto Di Cosmo, and Vincent Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. Ann. Pure Appl.
Logic, 141(1-2):35–50, 2006.
[15] Hugo Herbelin and Gyesik Lee. Forcing-based cut-elimination for Gentzen-style
intuitionistic sequent calculus. In Hiroakira Ono, Makoto Kanazawa, and Ruy J.
G. B. de Queiroz, editors, WoLLIC, volume 5514 of Lecture Notes in Computer
Science, pages 209–217. Springer, 2009.

15

[16] Danko Ilik. Formalisation of completeness for Kripke-CPS models, 2009.
http://www.lix.polytechnique.fr/~danko/code/kripke_completeness/.
[17] Danko Ilik. Constructive Completeness Proofs and Delimited Control. PhD thesis, École Polytechnique, October 2010.
[18] Danko Ilik, Gyesik Lee, and Hugo Herbelin. Kripke models for classical logic.
Annals of Pure and Applied Logic, 161(11):1367 – 1378, 2010. Special Issue:
Classical Logic and Computation (2008).
[19] Georg Kreisel. On weak completeness of intuitionistic predicate logic. J. Symb.
Log., 27(2):139–158, 1962.
[20] Saul Kripke. Semantical considerations on modal and intuitionistic logic. Acta
Philos. Fennica, 16:83–94, 1963.
[21] Damiano Macedonio and Giovanni Sambin. From meta-level to semantics via
reflection: a model for basic logic and its extensions. available from the authors.
[22] Chetan Murthy. Extracting Classical Content from Classical Proofs. PhD thesis,
Department of Computer Science, Cornell University, 1990.
[23] G. D. Plotkin. Call-by-name, call-by-value and the [lambda]-calculus. Theoretical Computer Science, 1(2):125–159, 1975.
[24] Clifford Spector. Provably recursive functionals of analysis: a consistency proof
of analysis by an extension of principles formulated in current intuitionistic mathematics. In Proc. Sympos. Pure Math., Vol. V, pages 1–27. American Mathematical Society, Providence, R.I., 1962.
[25] A. S. Troelstra and D. van Dalen. Constructivism in mathematics. Vol. I, volume
121 of Studies in Logic and the Foundations of Mathematics. North-Holland
Publishing Co., Amsterdam, 1988. An introduction.
[26] Wim Veldman. An intuitionistic completeness theorem for intuitionistic predicate
logic. J. Symb. Log., 41(1):159–166, 1976.
[27] A. J. Wilkie. On exponentiation - a solution to Tarski’s high school algebra problem. Technical report, Mathematical Institute, Oxford, UK, 2001.

16

