Spahn classical lambda calculus in modern dress (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

category: reference

J. M. E. Hyland, 27.11.2012, Classical lambda calculus in modern dress, arXiv:1211.5762

2. Algebraic theories

Let FF denote a standard skeleton of finite sets.

2.1 Algebraic theories as cartesian operads

Definition

An algebraic theory is defined to be a functor T:FSetT:F\to Set equipped with the structure of a cartesian operad:

  • We have sets T(n)T(n) of nn-ary multimaps (map with nn in-coming edges) with variable renamings (symmetric operad). (Think T(n)=C(*,,*;*)T(n)=C(*,\dots,*;*) as the hom space of the “underlying“ multicategory.)

  • There are projections pr 1,,pr nT(n)pr_1,\dots,\pr_n\in T(n) and in particular the identity idT(1)\id\in T(1). (One could also call the nn-th projection “nn-projection” or “nn-identity”.)

  • There are compositions T(m)×T(n) mT(n)T(m)\times T(n)^m\to T(n) which are associative, unital, compatible with projections, and natural in mm and nn.

Remark

The definition of algebraic theory encodes the rule rules of type formation:

ΓxΓt,Δs 1,Δs nΔt(s)\frac{}{\Gamma \vdash x}\;\;\;\frac{\Gamma \vdash t, \Delta\vdash s_1,\dots\Delta \vdash s_n}{\Delta\vdash t(s)}

where we interpret xx as to be declared in Γ\Gamma and t(s)t(s) as the result of substituting the strings of terms ss in tt.

(Paul Taylor writes

Γa:XΓ,x:Xt:YΓ(λx.t)a=t[a/x]\frac{\Gamma\vdash a:X\;\; \Gamma, x:X\vdash t:Y}{\Gamma\dashv (\lambda x.t)a=t[a/x]}

This is a beta-rule. )

2.2 Algebras for theories

2.3 The pre sheaf topos

2.4 Monads and Lawvere theories

(some comments on two classical approaches which are not used in the paper:

  1. monads on SetSet whose functor part is given by the coend formula T(A)= n𝒯(n)×A nT(A)=\int^n \mathcal{T}(n)\times A^n

  2. Lawvere theories)

3 The lambda calculus

Term-formation-in-context in Martin-Löf’s approach:

ΓtabΓuaΓtub\frac{\Gamma \vdash t\in a\Rightarrow b\;\Gamma\vdash \u\in a}{\Gamma \dashv tu\in b}
Γ,xasbΓλx.sab\frac{\Gamma, x\in a\vdash s\in b}{\Gamma \vdash\lambda x.s\in a\Rightarrow b}

computation rule:

(λx.s)u=s[u/x](\lambda x.s)u=s[u/x]

This means: an interpretation of lambda calculus is a cartesian multicategory with semiclosed structure.

Definition

Let LL be an algebraic theory.

(1) A semiclosed structure on LL is defined to be collection of retractions

L(n)L(n+1)L(n)L(n)\to L(n+1)\to L(n)

which is natural in nn and compatible with the actions

L(m)×L(n) mL(n)L(m)\times L(n)^m\to L(n)

and

L(m+1)×L(n) mL(n+1)L(m+1)\times L(n)^m\to L(n+1)

(2) A λ\lambda-theory is defined to be an algebraic theory LL equipped with a semi-closed structure.

Revision on November 29, 2012 at 04:58:50 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.