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

\begin{align*} \mathsf{expressions} &~ e ::= () \mid x \mid \lambda x:\tau.e \mid e_1~e_2 \mid n \mid e_1 \circ e_2 \mid \mathsf{left}_{\tau_1 + \tau_2} e \mid \mathsf{right}_{\tau_1 + \tau_2} e \mid \mathsf{case}~e_0~\mathsf{of}\{e_1 \mid e_2\} \mid (e_1, e_2) \mid \#1~ e \mid \#2~ e \\ \mathsf{types} &~ \tau ::= \mathsf{unit} \mid \mathsf{int} \mid \tau_1 \to \tau_2 \mid \tau_1 + \tau_2 \mid \tau_1 \times \tau_2 \end{align*}


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

Intuitively, \mathsf{case}~\mathsf{left}_{\mathsf{int}+\mathsf{unit}}~42~\mathsf{of}\{ \lambda x:\mathsf{int}.x^2 \mid \lambda x:\mathsf{unit}. 42 \} will match the \mathsf{left} term to the function \lambda x:\mathsf{int}.x^2 and reduce to


(\lambda x:\mathsf{int}.x^2)~(42)


which will output 42^2

on the other hand, \mathsf{case}~\mathsf{right}_{\mathsf{int}+\mathsf{unit}}~()~\mathsf{of}\{ \lambda x:\mathsf{int}.x^2 \mid \lambda x:\mathsf{unit}. 42 \} will reduce to

(\lambda x:\mathsf{unit}.42)~()


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

Furthermore, a tuple (e_1,e_2) will produce a product type \tau_1 \times \tau_2, 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.
\Gamma \vdash e : \tau


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

\frac{~}{\Gamma \vdash n : \mathsf{int}}\mbox{\textsc{T-Int}}


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

\frac{~}{\Gamma \vdash () : \mathsf{unit}}\mbox{\textsc{T-Unit}}


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

\frac{\Gamma(x) = \tau}{\Gamma \vdash () : \tau}\mbox{\textsc{T-Var}}


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

\frac{\Gamma \vdash e_1 : \mathsf{int} ~~~~ \Gamma \vdash e_2 : \mathsf{int}}{\Gamma \vdash e_1 \circ e_2 : \mathsf{int}}\mbox{\textsc{T-Op}}


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

\begin{align*} &\frac{~}{\Gamma \vdash n : \mathsf{int}}\mbox{\textsc{T-Int}} \\ \\ &\frac{~}{\Gamma \vdash () : \mathsf{unit}}\mbox{\textsc{T-Unit}} \\ \\ &\frac{\Gamma(x) = \tau}{\Gamma \vdash () : \tau}\mbox{\textsc{T-Var}} \\ \\ &\frac{\Gamma \vdash e_1 : \mathsf{int} ~~~~ \Gamma \vdash e_2 : \mathsf{int}}{\Gamma \vdash e_1 \circ e_2 : \mathsf{int}}\mbox{\textsc{T-Op}} \\ \\ &\frac{\Gamma, x:\tau \vdash e : \tau'}{\Gamma \vdash \lambda x:\tau . e : \tau'}\mbox{\textsc{T-Abs}} \\ \\ &\frac{\Gamma \vdash e_1 : \tau \to \tau' ~~~~ \Gamma \vdash e_2 : \tau}{\Gamma \vdash e_1 ~ e_2 : \tau'}\mbox{\textsc{T-App}} \\ \\ &\frac{\Gamma \vdash e : \tau_1}{\Gamma \vdash \mathsf{left}_{\tau_1 + \tau_2} ~ e : \tau_1 + \tau_2}\mbox{\textsc{T-Left}} \\ \\ &\frac{\Gamma \vdash e : \tau_2}{\Gamma \vdash \mathsf{right}_{\tau_1 + \tau_2} ~ e : \tau_1 + \tau_2}\mbox{\textsc{T-Right}} \\ \\ &\frac{\Gamma \vdash e_0 : \tau_1 + \tau_2 ~~~~ \Gamma \vdash e_1 : \tau_1 \to \tau ~~~~ \Gamma \vdash e_2 : \tau_2 \to \tau}{\Gamma \vdash \mathsf{case}~e_0~\mathsf{of}~\{e_1 \mid e_2\} : \tau}\mbox{\textsc{T-Case}} \\ \\ &\frac{\Gamma \vdash e_1 : \tau_1 ~~~~ \Gamma \vdash e_2 : \tau_2}{\Gamma \vdash (e_1, e_2) : \tau_1 \times \tau_2}\mbox{\textsc{T-Tuple}} \\ \\ &\frac{\Gamma \vdash e : \tau_1 \times e_2 : \tau_2}{\Gamma \vdash \#1~e : \tau_1 }\mbox{\textsc{T-\#1}} \\ \\ &\frac{\Gamma \vdash e : \tau_1 \times e_2 : \tau_2}{\Gamma \vdash \#2~e : \tau_2 }\mbox{\textsc{T-\#2}} \\ \\ \end{align*}

Reply to this post

Replies

Analogy between types and first order logic
posted by Lee
posted 170d 12h ago
Next, we say that \vdash e : \tau to mean that e has type \tau within the empty context. Since the empty context \varnothing is the bottom element, then if \vdash e : \tau implies that for all \Gamma, \Gamma \vdash e : \tau.

Finally, we say an expression e is well typed if there exists some type \tau such that \vdash e : \tau. For example, the program (\lambda x:\mathsf{unit}. x)~42 is not well typed since we can't apply 42 to a function expecting (). But the program (\lambda x:\mathsf{int}. x)~42 is well typed because we can build the derivation/proof tree of its typing:

\dfrac{ \dfrac{ \dfrac{[x:\mathsf{int}](x) = \mathsf{int}}{x:\mathsf{int} \vdash x : \mathsf{int}}\mbox{\textsc{T-Var}} }{\vdash \lambda x:\mathsf{int}. x : \mathsf{int} \to \mathsf{int}}\mbox{\textsc{T-Abs}} ~~~~ \dfrac{~}{\vdash 2 : \mathsf{int}}\mbox{\textsc{T-Int}} }{\vdash (\lambda x:\mathsf{int}. x)~42 : \mathsf{int}}\mbox{\textsc{T-App}}


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

Finally, we illustrate the analogy between types in \lambda^{\tau,+,\times} 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
\Gamma \vdash \phi


for some logical context \Gamma and some logical atom \phi, that if all of the logical elements within the context \Gamma = \{\psi_1, \psi_2, \cdots\} hold/are true, then we can conclude that \phi are also true.

Compare this to the type relation case where
\Gamma \vdash e : \tau


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

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
\frac{A,B,\Gamma \vdash \phi}{A \wedge B, \Gamma \vdash \phi}\wedge\mbox{\textsc{-Left}}~~~~\frac{\Gamma \vdash A ~~~~ \Gamma \vdash B}{\Gamma \vdash A \wedge B}\wedge\mbox{\textsc{-Right}}


these are both quite similar to a derived typing rule from #1, #2 and our \mbox{\textsc{T-Tuple}} rule
\frac{a:A,b:B,\Gamma \vdash e:\tau}{p:A \times B, \Gamma \vdash \mathsf{let}~p=(a,b)~\mathsf{in}~e:\tau}\times\mbox{\textsc{-Left}}~~~~\frac{\Gamma \vdash a:A ~~~~ \Gamma \vdash v:B}{\Gamma \vdash (a,b) :A \times B}\mbox{\textsc{T-Tuple}}


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

For the disjunction case,
\frac{\Gamma \vdash A}{\Gamma \vdash A + B} ~~~~ \frac{\Gamma \vdash B}{\Gamma \vdash A + B}\vee\mbox{\textsc{-Right}} ~~~~ \frac{A,\Gamma \vdash \phi ~~~~ B,\Gamma \vdash \phi}{A \vee B, \Gamma \vdash \phi}\vee\mbox{\textsc{-Left}}

is isomorphic to the typing rules for left and right terms
\frac{\Gamma \vdash e: A}{\Gamma \vdash \mathsf{left}_{A + B}~e : A + B} ~~~~ \frac{\Gamma \vdash e: B}{\Gamma \vdash \mathsf{right}_{A + B}~e : A + B}

and the derived case rule
\frac{a:A,\Gamma \vdash e_1 : \tau ~~~~ b:B,\Gamma \vdash e_2 : \tau}{s : A + B, \Gamma \vdash \mathsf{case}~s~\mathsf{of}~\{\lambda a:A.e_1 \mid \lambda b:B.e_2\} : \tau}\mbox{\textsc{T-Case}}


As an exercise to the reader, show the same isomorphism between A \to B and A \implies B.

This then suggests that if it's possible to construct a term in \lambda^{\tau,+,\times} that has a type \tau, then the derivation tree proving that \tau can be directly translated into first order logic as a proof of the logic analog of \tau \to_{CH-Isomorphism} \phi.
Use this to start your reply
Analogy between types and first order logic
posted by Lee
posted 170d 11h ago
Finally, let's illustrate the relationship between sums and products in terms of \vee,\wedge. 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 \forall A. \tau and \forall A. \phi and introduce the concept of logical and type variables A that can be bound to only one type/logical formula.

By demorgan's law, we have the equivalence in first order logic that
A \vee B \equiv \neg(\neg A \wedge \neg B)


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
A \vee B \equiv (A \implies \bot \wedge B \implies \bot) \implies \bot


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

A \vee B \equiv \forall \alpha. (A \implies \alpha \wedge B \implies \alpha) \implies \alpha


then a proof of this in \lambda^{\tau,+,\times,\forall} constitutes a program with the type
A + B \equiv \forall \alpha. (A \to \alpha \times B \to \alpha) \to \alpha


which gives a simple encoding of sum types as product types via the syntax and type derivation directed translation, with a type translation \mathcal{T} that I will specify later
\dfrac{\Gamma \vdash e_1 : \tau_1 \to \alpha ~~~~ \Gamma \vdash e_2 : \tau_2 \to \alpha ~~~~ \alpha' = \mathcal{T}[\alpha]} {\mathcal{E}[\mathsf{case}~e_0~\mathsf{of}\{e_1\mid e_2\}] = \mathcal{E}[e_0]_{\alpha'} ~ (\mathcal{E}[e_1], \mathcal{E}[e_2])}

\mathcal{E}[\mathsf{left}_{\tau_1 + \tau_2} ~ e] = \forall \alpha.\lambda p: \mathcal{T}[\tau_1] \to \alpha \times \mathcal{T}[\tau_2] \to \alpha. (\#1 p)~\mathcal{E}[e]

\mathcal{E}[\mathsf{right}_{\tau_1 + \tau_2} ~ e] = \forall \alpha.\lambda p: \mathcal{T}[\tau_1] \to \alpha \times \mathcal{T}[\tau_2] \to \alpha. (\#2 p)~\mathcal{E}[e]


and the rest of the \mathcal{E} is defined as the identity, where \mathcal{T}[\tau_1 + \tau_2] = \forall \alpha . (\mathcal{T}[\tau_1] \to \alpha \times \mathcal{T}[\tau_2] \to \alpha) \to \alpha) followed by the identity mapping as well.

For example, the program
\mathsf{case}~ (\mathsf{left}_{\mathsf{int} + \mathsf{unit}} ~ 42) ~\mathsf{of}~\{\lambda x:\mathsf{int}. x^2 \mid \lambda x:\mathsf{unit}. 42\}


will be transformed via the above translation to
\alpha = \mathsf{int}. \bigl(\lambda p. \mathsf{int} \to \alpha \times \mathsf{unit} \to \alpha. (\#1~ p)~ 42\bigr)~ (\lambda x:\mathsf{int}. x^2, \lambda x:\mathsf{unit}. 42)


Neat!
Use this to start your reply
Submit Reply
Title: Your Name:
Wrap equations in [EQ]equation here[/EQ] tags, and inline equations in [IEQ][/IEQ] tags.