We saw in the previous two sections that the new focus operator is equivalent to definition by description. This is more familiar, both in the sense of tradition, but also in that the requirements on its data are more idiomatic: a predicate with a unique numerical solution, rather than a term of type Σ2 X satisfying a strange equation. Indeed, this calculus seems to be a useful denotational basis for both mathematical and computational investigations: it plays a similar role to that of the class of total recursive functions, whilst being better both as a type theory and for computation.
As it stands, it does not meet the needs of mathematicians, who expect to be able to form subtypes by means of the axiom of comprehension and other constructions such as disjoint sums. Such subtypes, specified by a comprehension-like operation, but equipped with the subspace topology, will be added to the category in [B]. However, this is ignored by computation, i.e. by the reduction rules for the terms.
Topological ideas such as compact Hausdorff spaces are studied in [C][G], and the partial map classifier or lift X⊥ in [D][F].
Remark 11.1 For high-level computation, on the other hand, the calculus is already
a serviceable functional programming language.
It has as
Following Peter Landin [Lan64], it is useful to “sugar” λ-application (λ x.φ)a or plain substitution [a/x]*t, with syntax such as
| let x=a in t or t where x=a. |
The Y-combinator that we derived from the continuity axiom in Remark 2.6 provides recursively defined procedures. So
| letrec φ(x1,⋯,xn)=F in t, |
in which φ may be used in F as well as in t, is encoded as
| let φ = ∃ n. rec (n, ⊥, λ m φ x1⋯ xn. F) in t. |
The body F may contain the “recursive call” φ and its recursive arguments x1,⋯,xn; these are the variables bound by the λ within rec. The numerical variables n and m count the depth of the recursion, but their values are forgotten by ∃ n.
The development of mathematical and topological structures contributes Floyd–Hoare reasoning and special types such as X⊥ to the programming applications. However, by using mathematical intuitions to construct ℝ [I] and other objects, it will also provide methods of programming (i.e. algorithms) for problems where no order of evaluation is naturally apparent.
Remark 11.2 How could we then compile such a program?
As we have understood the calculi in this paper denotationally, let us first clarify what we mean by compilation and execution. In, for example, elementary algebra, we use the rules (such as distributivity) in whatever fashion seems best, to simplify the given complicated expression into a denotationally equivalent one that lies within a subclass of preferred forms. In doing this, we choose some amongst all valid reduction paths.
The objective may be “full” execution, in which we are satisfied with nothing less than an explicit number (assuming that the expression is of type ℕ), and thereby risk non-termination. Alternatively it may be to re-express the program in some simpler language, removing high-level features, but without actually doing the iterations. This translation is called compilation, and is required always to terminate. Sometimes compilation may use η-rules and reverse β-rules that would not be used in an execution strategy.
Remark 11.3 Without loss of generality, the term to be compiled is of type Σ,
since terms of higher type may be applied to free variables,
and a numerical term Γ⊢ t:ℕ
may be handled as Γ,m:ℕ⊢ m=t:Σ.
For example, a numerical function f:ℕ→ℕ
is treated in the form of its graph, n,m:ℕ⊢ m=f(n):Σ.
[Terms of other types are obtained by enclosing logical ones in
the n. or
λ x.]
Lemmas 9.2, 9.5 and 9.6 eliminate embedded descriptions and recursion of numerical type in favour of additional existentially quantified variables, so the numerical sub-terms that remain are ordinary expressions.
Suppose at first that the term doesn’t involve disjunction or recursion: any such sub-term is replaced by a logical variable and will be handled separately.
Since we have a fragment of the simply typed λ-calculus with some constants, the term strongly normalises. This eliminates λ-abstraction and application, which is a desirable property of our compiler, as both Abstract Stone Duality and the Continuation-Passing Style introduce numerous “administrative” λ-expressions of the form λφ.φ[a].
Any existential quantifiers may be moved to the front by renaming the bound variables (this uses the Frobenius law to get past ∧). What remains is either ⊤, ⊥, or a conjunction of sub-terms, each of which is either
The entire term may be existentially quantified over some numerical variables, effectively “hiding” them. This is a pure Prolog clause (apart from the free logical variables).
The numerical equations may be normalised by unification. The occurs check must be made, since logically (∃ n.n=f(n))≡⊥ if f is any non-trivial numerical expression in which the variable n is free. The result of unification serves as a pattern that the free numerical variables must satisfy; the pattern is incorporated into the head of the clause, and many of the hidden variables are eliminated in this process. The body consists of the other logical conjuncts.
We restore disjunction to the language by introducing a Prolog predicate-symbol for each ∨ sub-term, with a clause for each branch. In order to be denotationally equivalent to the original term, these disjuncts must in general be executed in parallel. This is because they may fail either finitely (because of a clash in unification) or infinitely by non-termination, whereas ∨ is meant to be commutative. In practice, the branches are usually guarded by patterns, all but one of which fail straight away.
The term rec(n,Z,λ m u.S) is treated like the disjunction
| (n=0∧ Z)∨(∃ m.n=m+1∧ S(m,u)) |
but with an actual link to rec(m,Z,λ m u.S) in place of u. The circular translation from programming language to our calculus and back therefore simply introduces a hidden variable n that counts the depth of the recursion. (There is a disjunct ⊥ that is redundant.)
For the most part, logical variables in the main program are bound to Prolog procedures, any free ones being (illegally) undefined procedure names. However, recursion at type ΣΣℕ or higher types does involve passing logical arguments to recursive procedures. In simple cases, this may be done by Gödel-numbering them, and in fact it is not difficult to write a self-interpreter for and in pure Prolog.
Remark 11.4
Turning from low- to high-level programming, what can we make
of Thielecke’s force operator? In our treatment, we insisted that
focus be accompanied by its side condition (that it only be applied
to primes), so maybe we are unable to interpret control operators.
But the difference is merely that we have investigated SC,
which includes general recursive function,
and argued that it should be used in place of C,
which only has primitive recursion.
The category HC with control operators is still there,
and HC≅HSC.
Its terms are interpreted contravariantly in C,
by means of a λ-translation which, when written on paper,
may seem complicated [Fis93, Section 4],
but is dissolved away by our λ-normalising compiler.
John Reynolds has given a nice historical survey of mathematical and computational calculi that use continuations [Rey93]; for a formal introduction to control operators, you should see the work cited there. Here, we shall just say something about the consequences of dropping the primality side-condition, by way of an introduction addressed to mathematical readers. Note that the programming language for HC that we’re about to describe is to be translated into the sober calculus, and is not an extension of it.
In return for allowing force to be used without restriction, we have to constrain the reduction rules in general, i.e. to impose an order of evaluation. We choose call by value, in which the argument a is reduced before the β-redex (λ x.φ)a, and unapplied abstractions λ x.φ are not reduced at all.
This means, in particular, that the argument of φ(forceP) gets evaluated before φ, turning the expression into Pφ. However, we must specify how much of the enclosing expression φ is to be consumed by this reduction. We do this by introducing another keyword, label, as a delimiter (it has no computational effect in itself). Since force may occur repeatedly, we must name the label that delimits each force. Assuming that neither F nor φ can be reduced on its own,
| F(labelk φ (forcek P)) reduces to F(Pφ). |
What has happened here, in programming terms? The part of the continuation (φ) that is bracketed by label and force has been given to P as an argument. Because of the call-by-value rules, φ does not get executed until P puts it into an active position in front of an argument. P may also duplicate or lose φ. When it has finished, P does not return in the normal way to its calling context (φ), but to F, i.e. to the position of the matching label. In other words, forcek jumps to labelk. Unless, that is, φ gets executed and itself performs a different jump.
Remark 11.5 Our compiler translated disjunction into alternative
Prolog clauses, which ought in general to be executed in
parallel. If, however, one branch fails finitely, it can
back-track to the point of choice, and proceed with another option.
Continuations provide the natural way in which to do this. Instead of having a single calling context φ to which it always returns normally, a sub-program that has a notion of finite failure can be supplied with two continuations, φ+ and φ−, which it may invoke respectively in the event of success and failure [Hay87, Thi01]. This translation is not the one that we obtain from disjunction (cf. Proposition 10.6), but does fall naturally out of the interpretation of coproducts (disjoint unions) in B 11.
Remark 11.6 There are several reasons why pure Prolog should arise as
the intermediate or object language of our compiler,
that is, that we use logic rather than functional programming.
Primarily, it is that we chose ΣX rather than X⊥
our basic type constructor.
Then terms Γ→ΣX are relations,
whereas those Γ→ X⊥ are partial functions.
However, it is a curious feature of Prolog that single clauses are static: the control and data-flow only acquire a direction when the clauses are put together into a whole program. This may perhaps be connected with the fact that it is a natural target of the continuation-passing style, i.e. that we are translating high-level programs that are themselves ambivalent about their direction.