Lambda Calculus

In type theory a function type can be constructed from(deconstructed to) an expression. function diagram

Type Theory rules for Lambda Calculus

 

Function Type

formation rule

Given any two types A and B we can form a function type A->B

right adjointA:Type   right adjointB:Type
right adjointA->B : Type

term introduction rule

assume a implies b

(given a proof of A we get a proof of B)

lambda abstraction:

Γ a:Aright adjointb:B   Γright adjointB:Type
Γright adjointλa.b : A -> B

term eliminator

Modus Ponens

application:

Γright adjointA->B:Type   Γright adjointa:A
Γright adjointf(a) : B

computation rule

substitution - in this case of a for x.

( λ x . b(x)) (a) ->β b(a)

we reduce this by substitution.

b[a/x]

Local completeness rule

eta reduction rule

M:A->B ->η λ x. M x

More about function type constructors (and deconstructors or eliminators) on page here.

Substitution

The computation rule above implements substitution. This computation rule is the term eliminator followed by the term introduction rule.

This is β-substitution, which is a change of the variable name.

Next

Modeling Computation

 


metadata block
see also:

 

Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.