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

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

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

2. Algebraic theories

An Let ~~algebraic~~ ~~theory~~ is a ~~functor~~ $Fin F Set \to Set$ ~~Fin~~ F ~~Set\to~~ ~~Set~~ . 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 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$ .

(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~~ Term-formation-in-context ~~formation~~ 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 03:07:33 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.