Computational Model Finite Automata

In type theory a function type can be constructed from(deconstructed to) an expression. [画像:function diagram]

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

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.