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

Showing changes from revision #3 to #4: Added | ~~Removed~~ | ~~Chan~~ged

category: reference

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

2. Algebraic theories

Let $F$ denote a standard skeleton of finite sets.

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

We have sets $T(n)$ of $n$ -ary multimaps (map with $n$ in-coming edges) with variable renamings (symmetric operad). (Think $T(n)=C(*,\dots,*;*)$ as the hom space of the “underlying“ multicategory.)
There are projections $pr_1,\dots,\pr_n\in T(n)$ and in particular the identity $\id\in T(1)$ . (One could also call the $n$ -th projection “ $n$ -projection” or “ $n$ -identity”.)
There are compositions $T(m)\times T(n)^m\to T(n)$ which are associative, unital, compatible with projections, and natural in $m$ and $n$ .

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

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

where we interpret $x$ as to be declared in $\Gamma$ and $t(s)$ as the result of substituting the strings of terms $s$ in $t$ .

(Paul Taylor writes

\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. )

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

monads on $Set$ whose functor part is given by the coend formula $T(A)=\int^n \mathcal{T}(n)\times A^n$
Lawvere theories)

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

\frac{\Gamma \vdash t\in a\Rightarrow b\;\Gamma\vdash \u\in a}{\Gamma \dashv tu\in b}

\frac{\Gamma, x\in a\vdash s\in b}{\Gamma \vdash\lambda x.s\in a\Rightarrow b}

computation rule:

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

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

Let $L$ be an algebraic theory.

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

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

which is natural in $n$ and compatible with the actions

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

and

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

(2) A $\lambda$ -theory is defined to be an algebraic theory $L$ 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.