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

2 hours 10 min ago

2 hours 21 min ago

3 hours 22 min ago

7 hours 54 min ago

9 hours 11 min ago

10 hours 10 min ago

10 hours 47 min ago

12 hours 14 min ago

13 hours 45 min ago

14 hours 11 min ago