Lambda the Ultimate

In a series of papers, Jean Goubault-Larrecq has established a relationship between modal logic systems and type systems for metaexpressions, i.e. (quasi-)quoted expressions. I will use a pseudo Lisp syntax and furthermore I will write quote for both quote and quasiquote. In such systems, if (has-type (quote x) (quote A)), then (has-type (quote (quote x)) (quote ([] A))), where [] is a modal operator. One can read "([] A)" as "a representation of an A". The unquote is the corresponding destructor.

It appears to me that modal operators are merely syntactic abbreviations for predicates on propositions, i.e., ([] A) is merely an abbreviation for (P (quote A)) where P is some corresponding predicate on propositions. For example, the modal operator in provability logics can be identified with the |- provability predicate: to express that A is provable one can write either (|- (quote A)), or ([] A). A proposition thus has type (quote (|- (quote bool))).

(By the way, if we treat predicates/sets as characteristic functions, then modal operators are really evaluators, and |- with two relands is an evaluator with an environment. A partially applied type-assignment relation (has-type (quote x)) then corresponds to a modal operator [(quote x)] that has a term as a parameter.)

The proof rules rules for minimal logic in their most basic form (with a single proposition instead of a context) look like the following:

(has-type (quote make-x) (quote (|- (quote P)))) 
(has-type (quote make-y) (quote (|- (quote Q))))
; ... other assumptions

(has-type (quote i→)
          (quote (∀ a (|- (quote bool))
                   (∀ b (|- (quote bool))
                     (→ (→ (|- a) (|- b))
                        (|- (quote (→ (unquote a) (unquote b)))))))))
(has-type (quote e→)
          (quote (∀ a (|- (quote bool))
                   (∀ b (|- (quote bool))
                     (→ (|- (quote (→ (unquote a) (unquote b))))
                        (→ (|- a) (|- b)))))))

Now it becomes clear that proof rules are the types of the constructors of the proofs (terms) in a language. For example, (e→ (quote (→ A B)) (quote A) (quote f) (quote x)) denotes (quote (f x)) The first two arguments are there because e→ is polymorphic, but they can be left implicit.

The written representation of an abstraction term is now problematic because the abstraction term contructor i→ takes a function of type (quote (→ (|- (quote A)) (|- (quote B)))) as argument, not a (sub)term. To write down a abstraction term we would have to write the written representation of a function. This implies it is impossible to write down abstraction terms.

We can resort to a trick to be able to write some abstraction terms indirectly. Here the substitution function comes to the rescue. Most generally, subst takes five arguments: (subst (quote A) (quote B) (quote x) (quote M) (quote N)). The two types (quote A) and (quote B) are given because subst is polymorphic and it must be specified what is the type of (quote x) on the one hand and (quote N) and (quote M) on the other hand. I will sometimes leave them implicit as in other situations.

Partially applying subst to four arguments, the resulting term has the required type (quote (→ (|- a) (|- b))). Thus the term (i→ (quote A) (quote B) (subst (quote A) (quote B) (quote x) (quote M))) is correctly typed and is a abstraction term that does what you expect.

This explains the strange shape of λ terms: a λ term is actually a macro (i.e. syntactic abbreviation) for a term that cannot be written, somewhat as follows (the output type b is inferred):

(defmacro λ (x a m))
  (i→ (subst a b x m)))

Note the absense of quotes in the body. Alternatively, we can add a new `λ reduction' rule (the output type b is inferred):

(∀ ... (→λ (quote (λ (unquote x) (unquote a) (unquote m)))
                  (i→ (subst a b x m))))

This explains the shape of the beta reduction rule:

(∀ ... (→β (e→ (quote (λ (unquote a) (unquote x) (unquote m))) n)
               (subst a b x m n)))

This is because this rule is merely a special case of a more general rule for beta reduction:

(∀ ... (→β (e→ (i→ f) n) (f n)))

or, even more generally,

(∀ ... (→β (e→ (i→ f)) f))

or even something like:

(∀ ... (→β (° e→ i→) id))

By the way, the type assignment rules then become:

(has-type (quote t-make-x) (quote (has-type make-x (quote P))))
(has-type (quote t-make-y) (quote (has-type make-y (quote Q))))
; ... other variable declarations
(has-type (quote ti→)
          (quote (∀ ...
                   (→ (→ (has-type x a) (has-type (f x) b))
                      (has-type (i→ f) (quote (→ (unquote a) (unquote b))))))))
(has-type (quote te→)
          (quote (∀ ...
                   (→ (has-type f (quote (→ (unquote a) (unquote b))))
                      (→ (has-type x a) (has-type (e→ f x) b))))))