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 `quote`

s 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))))))

## Recent comments

3 hours 11 min ago

15 hours 27 min ago

16 hours 20 min ago

16 hours 50 min ago

16 hours 58 min ago

17 hours 19 min ago

17 hours 20 min ago

17 hours 23 min ago

20 hours 55 min ago

21 hours 13 min ago