Computer Aided Formal Reasoning Fall, 1995 Lecture notes 16 Judith Underwood

Much of the text of this note is lightly edited from old papers of mine and/or my thesis. Hence, the tone is slightly more formal than that of previous notes, and is a bit more wordy.

1 Typing of nonlocal control

Control operators were introduced to functional languages for reasons of efficiency. The use of continuations to describe nonlocal control flow can avoid the need to unwind deep layers of recursive calls when a result is found. However, they can be used to write very complex code – they are essentially a functional goto. Reasoning about control operators has been an important area of research in functional programming.

As it happens, a type-theoretic approach to reasoning about control operators also solves another problem – how to extend the Curry-Howard isomorphism to classical logic. The question is, “Can we extract a sensible computation from a proof which uses classical reasoning?” It turns out that some nonlocal control operators can be given types of classical axioms – in particular, axioms strong enough to prove all of classical logic when added to intuitionistic logic. Furthermore, the resulting programs extracted from classical proofs actually have the correct computational behaviour (within some limits).

1.1 Evaluation rules for call/cc

We begin by looking at the computational meaning of call/cc, a particular nonlocal control operator used in the language Scheme. First, we give some formal evaluation rules; then we’ll look at some examples.

Following the example of [2], we present the operational semantics as a set of rules representing the transition function of a term rewriting machine. We use their notion of a continuation point to represent the continuation object; however, since we do not fix an evaluation order, we shall use a more general notion of evaluation context (the analogous “applicative contexts” defined in [2] are defined for a particular evaluation order ). An evaluation context is a term with a hole in it, such that the hole is not within the scope of any binding operators. A program not in normal form can be split into an evaluation context and a redex. We use the notation E[R] for such a program, where E[] is the evaluation context and R is the redex. A continuation point is an evaluation context tagged with p. If E[R] is a program of type φ and R is of type α, then ⟨p, E[]⟩ is a continuation point which may be applied to any term of type α to produce a program of type φ.

The language we use is somewhere between λ-calculus and Lego. The reduction rules for terms are:

E[(λx.t)a] ↦ E[t[x := a]]
E[or elim(inl(a); λu.t_{1}; λv.t_{2})] ↦ E[t_{1}[u := a]]
E[or elim(inr(b); λu.t_{1}; λv.t_{2})] ↦ E[t_{2}[v := b]]
E[call/cc(λk.t)] ↦ E[t[k := ⟨p, E[]⟩]]
E[(⟨p, E_{0}[]⟩)a] ↦ E_{0}[a]

Another way of looking at this is to add an extra operator A, read abort, and consider a continuation ⟨p, E[]⟩ as a function λx.AE[x]. We then add a reduction rule:

E[AE_{0}[M]] ↦ E_{0}[M]

We will use this formulation below.

1.1.1 Example

Let us consider an example of the use of call/cc to increase the efficiency of a functional program. Suppose we wish to write a function which takes the product of all the natural numbers in a list. Such a function could be written:

list rec one

λhd:nat.λtail:list nat.λtail prod:nat (times hd tail prod)

Recall that this is quite inefficient if the list contains zero. A slightly more efficient version is:

list rec one

λhd:nat.λtail:list nat.λtail prod:nat if zero hd zero (times hd tail prod)

If we apply this to a list (two zero three …), the term reduces as follows:

(list rec one (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd zero (times hd tail prod))) (two zero three …) ⇝(if zero two zero

(times two (list rec one (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd zero (times hd tail prod)) (zero three …)) )

⇝ (times two (list rec one (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd zero (times hd tail prod)) (zero three …))) ⇝ (times two ( if zero zero zero

(times zero (list rec one (λhd:nat.λtail:list nat.λtail prod:nat if zero hd zero (times hd tail prod)) (three …))) ))

⇝ (times two zero)

But this is still not ideal, since the multiplication is still performed for everything leading up to the zero in the list. What we really want is to return zero as soon as we encounter it in the list. This is a nonlocal return, since we avoid unwinding back through the recursive calls. We can do this using call/cc:

call/cc (λk.list rec one

λhd:nat.λtail:list nat.λtail prod:nat if zero hd (k zero) (times hd tail prod)

If we apply this to the list (two zero three …), the term reduces:

(call/cc …)(two zero three …) ⇝ (list rec one (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd ((λx.Ax) zero) (times hd tail prod))) (two zero three …)

⇝(if zero two ((λx.Ax) zero)

(times two (list rec one (λhd:nat. λtail:list nat. λtail prod:nat

if zero hd ((λx.Ax) zero) (times hd tail prod)) (zero three …)) ))

⇝ (times two (list rec one (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd ((λx.Ax) zero) (times hd tail prod)) (zero three …)))

⇝ (times two ( if zero zero ((λx.Ax) zero)

(times zero (list rec one (λhd:nat.λtail:list nat.λtail prod:nat if zero hd ((λx.Ax) zero) (times hd tail prod)) (three …))) ))

⇝ (times two ((λx.Ax) zero)) ⇝ (times two (Azero)) ⇝ zero

Here, the context of the call/cc was empty. If we had encountered this term inside some other context, say

(plus two (call/cc (λk. …)))

the continuation would have been

λx. A(plus two x)

1.2 Call/cc as a classical operator

In order to extend the “proofs as programs” principle to classical proofs, we must find a way of representing classical reasoning computationally. To do this, we must examine how classical reasoning differs from intuitionistic reasoning. The law of the excluded middle, i.e. the axiom P ∨¬P, is often considered the essence of the difference between classical and intuitionistic logic. However, proof theoretically this is not the case. By examining the rules for both intuitionistic and classical sequent calculus from a computational point of view, it becomes clear that the only rule which is substantially different is the rule for arrow-introduction on the right.

In Gentzen’s original presentation of the sequent calculus [4], the only difference between the calculus for intuitionistic logic and that for classical logic is the number of formulas allowed on the right side of the sequent. Here, we give an abbreviated version of the calculus for formulas containing → and ∨.

{Γ, A ⊢ B, Δ \atop Γ ⊢ A → B, Δ} {Γ ⊢ A, Δ \atop Γ ⊢ A ∨ B, Δ} {Γ ⊢ B, Δ \atop Γ ⊢ A ∨ B, Δ}

{Γ ⊢ A Γ, B ⊢ Δ \atop Γ, A → B ⊢ Δ}  {Γ, A ⊢ Δ Γ, B ⊢ Δ \atop Γ, A ∨ B ⊢ Δ}

We also have the cut rule:

{Γ ⊢ A Γ, A ⊢ Δ \atop Γ ⊢ Δ}

For intuitionistic logic, at most one formula is allowed in the conclusion. For classical logic, any finite number of formulas is permitted. So, while the intuitionistic interpretation of

Γ ⊢ A

is “Under the set of assumptions Γ we can prove the formula A,” the classical sequent

Γ ⊢ Δ

is interpreted as “If all formulas in Γ are true, then some formula A in Δ must be true.” In classical sequent calculus, then, there are multiple possible conclusions of the sequent and it is not necessary to demonstrate which one has been proved. In other words, the formulas in Δ form an implicit classical disjunction.

However, close inspection of the classical rules reveals that most can be interpreted constructively. That is, given a rule

{Γ ⊢ Δ \atop Γ′ ⊢ Δ′}

if we have a constructive proof of the hypothesis sequent, i.e. under the set of assumptions Γ we can prove constructively the disjunction of the formulas in Δ, then under hypotheses Γ′ we can prove, also constructively, the disjunction of the formulas in Δ′.

This is true despite the fact that we may have more than one formula on the right side of the turnstile. For, if a sequent Γ ⊢ Δ is constructively provable, given proofs of the formulas in Γ we will be able to determine which formula in Δ is proved. This is usually enough to allow us to determine which formula on the left of the conclusion sequent is proved.

For example, consider the rule for ∨ introduction on the left. Since many people think of the difference between classical and intuitionistic logic as resting in the behaviour of disjunction, it is somewhat surprising that the classical rule for disjunction is really constructive. The rule is

{Γ ⊢ A, Δ \atop Γ ⊢ A ∨ B, Δ}

If we have a constructive proof of Γ ⊢ A, Δ, then we have a function from elements of the types in Γ to the disjoint union type A ∨ ⋁ Δ. Thus, if we apply this function to particular elements of the types in Γ, we can determine the type of the result within the disjunction.

Given this function, it is easy to construct a function with the type corresponding to the conclusion of the sequent. The only modification is that if the result of the first function is of type A within the disjunction, it is injected to the type A ∨ B.

Even the structural rules can be interpreted constructively in this way. The only rule which cannot be constructively interpreted is the rule of arrow introduction on the left:

{Γ, A ⊢ B, Δ \atop Γ ⊢ A → B, Δ}

Since we may have satisfied the hypothesis sequent by proving something in Δ, and we may have used the assumption A, we cannot be certain that we can still prove anything in Δ. Nor can we prove A → B, since we may not have proved B in the hypothesis sequent. It is only in the computational content of this sequent that the call/cc operator appears. Call/cc can be typed with the classical tautology

((α → ⊥) → α) → α,

which is a form of Peirce’s law. This formula is not provable constructively. Furthermore, when it is added to constructive propositional logic as an axiom, the result is classical propositional logic.

We gave evaluation rules for call/cc in the last section. Here, we will explain the general behaviour of the operator in this setting by returning to the rule for arrow introduction. For simplicity, let us consider the case where Γ is empty, so the rule is

{A ⊢ B, Δ \atop ⊢ A → B, Δ}

Suppose we are given a constructive witness for the premise of the rule, i.e. a function f of type A → B ∨ ⋁ Δ. If we treat disjunction constructively, in order to provide a witness to A → B ∨ ⋁ Δ we must produce a term which is a witness to either A → B or to ⋁ Δ. However, we do not have enough information to provide this witness without a witness for A. To solve this dilemma, we use call/cc to define a term which, when evaluated, first appears to provide a witness w_{A→B} to A → B. However, this term also contains the current continuation, i.e. a description of the state of the computation at the point where this decision is made. Should the computation proceed in such a way that this witness w_{A→B} is applied to a term a type A, the term then applies f (the witness to the premise of the rule) to a obtain a term in B ∨ ⋁ Δ. If this term is actually in B, then it is returned and the computation proceeds. In this case, the term w_{A→B} given for A → B actually behaves as a normal witness for A → B, as expected. However, if the result of applying the witness to the premise has the type of a formula in ⋁ Δ, we apply the continuation which was captured at the time the decision between A → B ∨ ⋁ Δ was evaluated to return to this point in the computation with new information – namely, the inhabitant of ⋁ Δ.

To take a more concrete example, consider the law of the excluded middle, or A ∨ ¬A. Since ¬A = A → ⊥, the proof of this in Gentzen’s sequent calculus involves the following use of arrow introduction:

{A ⊢ ⊥, A \atop ⊢ A → ⊥, A}

The evaluation of the term inhabiting A → ⊥ ∨ A captures the current context and produces an alleged inhabitant of A → ⊥. Should this function ever be applied, however, it must be applied to something of type A. At this point, the continuation is applied to return the computation to the context in which the decision A → ⊥ ∨ A was made, and the computation continues with the newly supplied evidence for A instead of A → ⊥.

The previous example demonstrates that the evaluation of terms containing call/cc is generally only useful when they are in the context of a term which is expected to produce data. Although the term for A → ⊥ ∨ A can be evaluated on its own, it cannot be evaluated to a form which does not contain continuations. However, when it is used in a term which produces, say, a natural number, the term performs useful computation.

1.3 Extracting programs from classical proofs

Recall that the case of arrow introduction on the right where there is more than one formula on the right is the only one where assuming the hypothesis is constructive does not imply the conclusion is constructive. It is here we must introduce call/cc.

f : Γ, A ⊢ B, Δ
λg.call/cc(λh.inl(λx.or elim((f(g))x; λu.u; λv.absurd elim(h(inr(v)))))) : Γ ⊢ A → B, Δ

(This term is made more complex by the fact that we are using a language associated with natural deduction to describe a sequent calculus rule.) To see the intuition behind this term, we consider how it will be used in computation. Suppose Γ is empty, so that we have

call/cc(λh.inl(λx.or elim(f(x); λu.u; λv.absurd elim(h(inr(v))))))

as a closed term of type (A → B)∨Γ. If we use this term in a computation of a piece of printable data (i.e. a number, a list, etc.), we must perform a case split (via or elim) to eliminate the disjunction. When the term is evaluated, h is bound to the current continuation and we have

inl(λx.or elim(f(x); λu.u; λv.absurd elim(h(inr(v)))))

as the term of type (A → B) ∨ Γ. So, in the case split, we take the branch for A → B with the function

λx.or elim(f(x); λu.u; λv.absurd elim(h(inr(v))))

as our purported inhabitant of the type A → B. Now suppose this function is applied to a term a of type A. Applying the function f from the hypothesis of the sequent to a, we have an element of B ∨ Δ. Should this actually be of type B, then we return that value. If not, we have an inhabitant v of Δ. We then return the computation to the stage at which we took the case split for (A → B) ∨ Δ by applying the continuation h to our new evidence for (A → B) ∨ Δ, namely, inr(v) where v is the inhabitant of Δ produced by f(a). Thus, the continuation operator allows the computation to switch paths when the computation produces further evidence which determines which of the disjuncts is proved.

2 References

Since the discovery of a classical typing for the control operator C by Griffin [5], foundational work has been done in expressing these computations as programs in a typed lambda calculus extended by nonlocal control operators. In his thesis [6], Murthy showed that a classical proof of a Π_{2}^{0} sentence φ can be interpreted as a program in an extended lambda calculus which meets the specification φ. He also demonstrated that translations from classical to intuitionistic logic correspond to continuation-passing style translations of programs with control operators to programs without. In [7], Murthy showed that this interpretation gives a computational meaning to Friedman’s conservative extension theorem for classical over constructive arithmetic for Π_{2}^{0} sentences (in [3]).

Barbanera and Berardi have also worked in this area, and have proved a strong normalization result for a language including the control operator C in [1]. Unfortunately, they have some substantial restrictions on the types allowed in the language.

References

[1] Franco Barbanera and Stefano Berardi. Continuations and simple types: a strong normalization result. manuscript, 1992.

[2] Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52:205–237, 1987.

[3] H. Friedman. Classically and intuitionistically provably recursive functions. In D.S. Scott and G.H. Muller, editors, Higher Set Theory, Lecture Notes in Mathematics, Vol. 669, pages 21–28. Springer-Verlag, 1978.

[4] Gerhard Gentzen. Investigations into logical deduction (1934). In M. Szalo, editor, The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969.

[5] T. Griffin. A formulas-as-types notion of control. In Proc. of the Seventeenth Annual Symp. on Principles of Programming Languages, pages 47–58, 1990.

[6] C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, Dept. of Computer Science, 1990. (TR 89-1151).

[7] C. Murthy. An evaluation semantics for classical proofs. In Proc. of Sixth Symp. on Logic in Comp. Sci., pages 96–109. IEEE, Amsterdam, The Netherlands, 1991.