Infrequently Asked Questions

• How do I code a loop using ML datatypes?
• How do I add top and bottom to Gentzen's LK?

How do I code a loop using ML datatypes?

ML-style algebraic datatypes can be used to write non-terminating recursive loops, even without the use of fun (Standard ML) or rec. Note that this is impossible in System F, the type theory on which ML is loosely based. The trick is demonstrated below.

 
(* Bar's sole constructor, bar, contains a
   "negative occurrence" of Bar *)
datatype Bar = bar of Bar -> Bar

(* self_applier b applies the function
   embedded in b to b itself *)
val self_applier: Bar -> Bar =
  fn (b: Bar) => (case b of bar f => f b)

(* loop finishes "tying the knot" *)
val loop = self_applier (bar self_applier) 
  

The existence of such loops means that ML cannot be considered a logic via the Curry-Howard isomorphism. Such loops may be eliminated by forcing all datatypes to have strictly positive constructors.

How do I add top and bottom to Gentzen's LK?

Gerhard Gentzen's system LK is the prototypical classical sequent calculus. Wikipedia's Sequent Calculus article provides a good overview, as does Chapter 3 of Jean-Yves Girard's The Blind Spot.

LK includes a built-in negation operator, ¬P meaning “not P,” but does not contain symbols for the propositions ⊤, “true” or ⊥, “false.” It's occasional useful to talk about these, but it is not a priori clear that they are sound additions to LK.

Intuitionistic sequent systems, such as Gentzen's LJ, do not include negation directly and instead define ¬P as P ⊃ ⊥, “P implies false.” Of course this requires that ⊤ and ⊥ be built-in. LJ uses the following axioms.

There are two ways to add this to LK. The first is to augment LK's syntax with ⊤ and ⊥, and assert their axioms by fiat. We would then want to prove that the resulting system is sound by checking the relevant cases of the cut elimination theorem. This is hard. An easier approach is to instead define the new symbols by

With these definitions we can construct LK derivations showing that ⊤ and ⊥ satisfy the LJ-style axioms.

The derivations above, with our definitions of ⊥ and ⊤, show ⊥ ⊢ and ⊢ ⊤. Because this was all done within LK, we don't need to worry about reproving cut elimination.