Analogy between types and first order logic
posted by Lee
Suppose we have a simply typed lambda calculus core
whose expressions and types are defined inductively as

Here, the symbolic variables x represents variable names, n as integer literals, and () is the "null" element associated with the type. An abstraction, such as some identity function , will have a type (note that types are nominal only in the case of evaluation) of

Intuitively, will match the term to the function and reduce to

which will output

on the other hand, will reduce to

which produces 42. This then means that the left/right term produces a sum type

Furthermore, a tuple will produce a product type , and the "projection" operators #1 and #2 will take the first and the second elements out of that tuple respectively.

This then lends to a set of inductively define typing relation.

to mean that "e has type in the context/environment/type-mapping ", where is a mapping between variable names and types (). This may seem a bit mysterious, so let's look at a simple example.

This says that without any restrict, it will always be true that for any environment , an integer literal in our program (such as 42) will have a type of . The right-hand side names this inference rule. This seems reasonable. We also define the analogue for unit types

Next, let's define the rule for variables. Recall that is a mapping between variables and types, well

For numerical operations, we would require that is an integer only if both are themselves integers.

notice here that our typing relation here is defined "recursively" on itself. That is, in order to find the type of , we first need to find and verify that both the types of are integers as well. Let's now define all of our typing relations

### Replies

Analogy between types and first order logic
posted by Lee
Next, we say that to mean that e has type within the empty context. Since the empty context is the bottom element, then if implies that for all , .

Finally, we say an expression is well typed if there exists some type such that . For example, the program is not well typed since we can't apply 42 to a function expecting (). But the program is well typed because we can build the derivation/proof tree of its typing:

It also happens that these rules, in conjunction with the natural operational semantics defined for this system of simply typed lambda calculus , is sound. Soundness (in the case of this is equivalent to normalization) essentially says that well typed programs do not get stuck.

Finally, we illustrate the analogy between types in and first order logic.

It was noticed some time ago that the judgements within first order constructive/intuitionistic logic look REALLY REALLY similar to judgements for our typing relation. In first order logic, we say

for some logical context and some logical atom , that if all of the logical elements within the context hold/are true, then we can conclude that are also true.

Compare this to the type relation case where

to mean that given the inputs and an expression (such that we can transform these two into a collection of type judgements), then we can satisfy the relation .

Under these same interpretations however, we can get an isomorphic set of rules. For example, the rules for the left/right conjunction rules are respectively

these are both quite similar to a derived typing rule from #1, #2 and our rule

similarly for sum types and function types w.r.t to disjunction and implications

For the disjunction case,

is isomorphic to the typing rules for left and right terms

and the derived case rule

As an exercise to the reader, show the same isomorphism between and .

This then suggests that if it's possible to construct a term in that has a type , then the derivation tree proving that can be directly translated into first order logic as a proof of the logic analog of .
Analogy between types and first order logic
posted by Lee
Finally, let's illustrate the relationship between sums and products in terms of . In order to do this fully, we need to extend our SLTC with polymorphic universal types and our base order logic into second order constructive logic extended with universal quantifiers. Assume for now that both have the form and and introduce the concept of logical and type variables that can be bound to only one type/logical formula.

By demorgan's law, we have the equivalence in first order logic that

Now, negation itself isn't actually considered in the subset of the logical system we're working with, so we need to rewrite them into

where is defined as logical falsity. It's impossible to prove the above directly, but we can rewrite it into an equivalent form if we consider one possible isoforms to be and rewrite the scope of these universals to go to the same thing

then a proof of this in constitutes a program with the type

which gives a simple encoding of sum types as product types via the syntax and type derivation directed translation, with a type translation that I will specify later

and the rest of the is defined as the identity, where followed by the identity mapping as well.

For example, the program

will be transformed via the above translation to

Neat!