Just Typed Lambda Calculus

Simply typed lambda calculus ( simple typed lambda calculus , lambda calculus with simple types , system $\lambda ^{\rightarrow }$ ${\ displaystyle \ lambda ^ {\ rightarrow}}$ $\ lambda ^ {\ rightarrow}$ ) Is a system of typed lambda calculus in which a special "arrow" type is assigned to lambda abstractions. This system was proposed by Alonzo Church in 1940 ^[1] . For a close to lambda calculus formalism of combinatorial logic, a similar system was considered by Haskell Curry in 1934 ^[2] .

Content

Formal Description

Type and term syntax

In the basic version of the system $\lambda ^{\rightarrow }$ ${\ displaystyle \ lambda ^ {\ rightarrow}}$ types are constructed from a set of variables using a single binary infix constructor $\rightarrow$ ${\ displaystyle \ rightarrow}$ . By tradition, Greek letters are used for type variables, and the operator $\rightarrow$ ${\ displaystyle \ rightarrow}$ consider right associative, that is $\alpha \rightarrow \beta \to \gamma$ ${\ displaystyle \ alpha \ rightarrow \ beta \ to \ gamma}$ is short for $\alpha \rightarrow (\beta \to \gamma )$ ${\ displaystyle \ alpha \ rightarrow (\ beta \ to \ gamma)}$ . Letters from the second half of the Greek alphabet ( $\sigma$ ${\ displaystyle \ sigma}$ , $\tau$ ${\ displaystyle \ tau}$ , etc.) are often used to denote arbitrary types, not just type variables.

There are two versions of a simply typed system. If the terms used are the same terms as in the typeless lambda calculus , then the system is called implicitly typed or typed according to Curry . If the variables in lambda abstraction are annotated with types, then the system is called explicitly typed or typed according to Church . As an example, we give an identical function in the Curry style: $\lambda x.~x$ ${\ displaystyle \ lambda x. ~ x}$ , and in Church style: $\lambda x\!:\!\alpha .~x$ ${\ displaystyle \ lambda x \!: \! \ alpha. ~ x}$ .

Reduction Rules

The reduction rules do not differ from the rules for the typeless lambda calculus . $\beta$ ${\ displaystyle \ beta}$ reduction is determined by substitution

(\lambda x\!:\!\sigma .~M)~N\ \to _{\beta }\ M[x:=N]

{\ displaystyle (\ lambda x \!: \! \ sigma. ~ M) ~ N \ \ to _ {\ beta} \ M [x: = N]}

.

$\eta$ ${\ displaystyle \ eta}$ reduction is defined as

\lambda x\!:\!\sigma .~M~x\ \to _{\eta }\ M

{\ displaystyle \ lambda x \!: \! \ sigma. ~ M ~ x \ \ to _ {\ eta} \ M}

.

For $\eta$ ${\ displaystyle \ eta}$ reduction required that the variable $x$ ${\ displaystyle x}$ was not free in terma $M$ ${\ displaystyle M}$ .

Typing contexts and typing assertions

A context is a set of statements about typing variables separated by commas, for example,

f\!:\!(\beta \to \gamma ),g\!:\!(\alpha \to \beta ),x\!:\!\alpha

{\ displaystyle f \!: \! (\ beta \ to \ gamma), g \!: \! (\ alpha \ to \ beta), x \!: \! \ alpha}

Contexts are usually denoted in capital Greek letters: $\Gamma ,\Delta$ ${\ displaystyle \ Gamma, \ Delta}$ . In a context, you can add a “fresh” variable for this context: if $\Gamma$ ${\ displaystyle \ Gamma}$ - a valid context that does not contain a variable $x$ ${\ displaystyle x}$ then $\Gamma ,x\!:\!\alpha$ ${\ displaystyle \ Gamma, x \!: \! \ alpha}$ - also a valid context.

The general form of a typing statement is as follows:

\Gamma \vdash M\!:\!\sigma

{\ displaystyle \ Gamma \ vdash M \!: \! \ sigma}

It reads as follows: in context $\Gamma$ ${\ displaystyle \ Gamma}$ term $M$ ${\ displaystyle M}$ has type $\sigma$ ${\ displaystyle \ sigma}$ .

Typing Rules (Church)

In a simply typed lambda calculus, types are assigned to terms according to the rules below.

Axiom. If the variable $x$ ${\ displaystyle x}$ assigned in context type $\sigma$ ${\ displaystyle \ sigma}$ then in this context $x$ ${\ displaystyle x}$ has type $\sigma$ ${\ displaystyle \ sigma}$ . In the form of an output rule:

{x\!:\!\sigma \in \Gamma } \over {\Gamma \vdash x\!:\!\sigma }

{\ displaystyle {x \!: \! \ sigma \ in \ Gamma} \ over {\ Gamma \ vdash x \!: \! \ sigma}}

Introduction rule $\rightarrow$ ${\ displaystyle \ rightarrow}$ . If in some context extended by the statement that $x$ ${\ displaystyle x}$ has type $\sigma$ ${\ displaystyle \ sigma}$ term $M$ ${\ displaystyle M}$ has type $\tau$ ${\ displaystyle \ tau}$ , then in the mentioned context (without $x$ ${\ displaystyle x}$ ), lambda abstraction $\lambda x\!:\!\sigma .~M$ ${\ displaystyle \ lambda x \!: \! \ sigma. ~ M}$ has type $\sigma \to \tau$ ${\ displaystyle \ sigma \ to \ tau}$ . In the form of an output rule:

{\Gamma ,x\!:\!\sigma \vdash M\!:\!\tau } \over {\Gamma \vdash (\lambda x\!:\!\sigma .~M)\!:\!(\sigma \to \tau )}

{\ displaystyle {\ Gamma, x \!: \! \ sigma \ vdash M \!: \! \ tau} \ over {\ Gamma \ vdash (\ lambda x \!: \! \ sigma. ~ M) \! : \! (\ sigma \ to \ tau)}}

Delete rule $\rightarrow$ ${\ displaystyle \ rightarrow}$ . If in some context the term $M$ ${\ displaystyle M}$ has type $\sigma \to \tau$ ${\ displaystyle \ sigma \ to \ tau}$ , and the term $N$ ${\ displaystyle N}$ has type $\sigma$ ${\ displaystyle \ sigma}$ then application $M N$ ${\ displaystyle M ~ N}$ has type $\tau$ ${\ displaystyle \ tau}$ . In the form of an output rule:

{\Gamma \vdash M\!:\!(\sigma \to \tau )\quad \Gamma \vdash N\!:\!\sigma } \over {\Gamma \vdash (M~N)\!:\!\tau }

{\ displaystyle {\ Gamma \ vdash M \!: \! (\ sigma \ to \ tau) \ quad \ Gamma \ vdash N \!: \! \ sigma} \ over {\ Gamma \ vdash (M ~ N) \ !: \! \ tau}}

The first rule allows you to assign a type to free variables, setting them in context. The second rule allows you to typify a lambda abstraction with an arrow type, removing the variable associated with this abstraction from the context. The third rule allows you to typify the application (application), provided that the left applicant has a suitable arrow type.

Examples of typing assertions in Church style:

x\!:\!\alpha \vdash x\!:\!\alpha

{\ displaystyle x \!: \! \ alpha \ vdash x \!: \! \ alpha}

(axiom)

\vdash (\lambda x\!:\!\alpha .~x)\!:\!(\alpha \to \alpha )

{\ displaystyle \ vdash (\ lambda x \!: \! \ alpha. ~ x) \!: \! (\ alpha \ to \ alpha)}

(introduction

\rightarrow

{\ displaystyle \ rightarrow}

)

f\!:\!(\beta \to \gamma \to \delta ),y\!:\!\beta \vdash (f~y)\!:\!(\gamma \to \delta )

{\ displaystyle f \!: \! (\ beta \ to \ gamma \ to \ delta), y \!: \! \ beta \ vdash (f ~ y) \!: \! (\ gamma \ to \ delta) }

(removal

\rightarrow

{\ displaystyle \ rightarrow}

)

Properties

Just a typed system has the property of typical security: with $\beta$ ${\ displaystyle \ beta}$ -reductions, the type of lambda term remains unchanged, while typing itself does not interfere with the advancement of calculations.
In 1967, William Tate proved ^[3] that $\beta$ ${\ displaystyle \ beta}$ -reduction for a simply typed system has the property of strong normalization: any admissible term in a finite number $\beta$ ${\ displaystyle \ beta}$ reductions is reduced to a single normal form. Consequently $\beta \eta$ ${\ displaystyle \ beta \ eta}$ -equivalence of terms is solvable in this system.
The Curry-Howard isomorphism simply associates a typed lambda calculus with the so-called “minimal logic” (a fragment of the intuitionistic propositional logic of statements that includes only implication ): the populated types are exactly tautologies of this logic, and the terms correspond to evidence written in the form of a natural conclusion.

Notes

↑ A. Church. A Formulation of the Simple Theory of Types // J. Symbolic Logic. - 1940. - S. 56-68 .
↑ HB Curry. Functionality in Combinatory Logic // Proc Natl Acad Sci USA. - 1934. - S. 584-590 .
↑ WW Tait. Intensional Interpretations of Functionals of Finite Type I // J. Symbolic Logic. - 1967 .-- T. 32 (2) .

Literature

Pierce, Benjamin C. Types and Programming Languages. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Translation into Russian: Pierce B. Types in programming languages. - Dobrosvet , 2012 .-- 680 p. - ISBN 978-5-7913-0082-9 .
Barendregt, Henk. Lambda Calculi with Types // Handbook of Logic in Computer Science. - Oxford University Press, 1992 .-- T. II . - S. 117-309 .

[Church40-1] A. Church. A Formulation of the Simple Theory of Types // J. Symbolic Logic. - 1940. - S. 56-68 .

[Curry34-2] HB Curry. Functionality in Combinatory Logic // Proc Natl Acad Sci USA. - 1934. - S. 584-590 .

[Tait67-3] WW Tait. Intensional Interpretations of Functionals of Finite Type I // J. Symbolic Logic. - 1967 .-- T. 32 (2) .