category: reference J. M. E. Hyland, 27.11.2012, Classical lambda calculus in modern dress, [ arXiv:1211.5762](http://arxiv.org/abs/1211.5762) ## 2. Algebraic theories Let $F$ denote a standard skeleton of finite sets. ### 2.1 Algebraic theories as cartesian operads +-- {: .num_lemma} ###### Definition 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$. =-- +-- {: .num_lemma} ###### Remark The definition of *algebraic theory* encodes the 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. ) ### 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 $Set$ whose functor part is given by the coend formula $T(A)=\int^n \mathcal{T}(n)\times A^n$ 1. Lawvere theories) ## 3 The lambda calculus 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*. +--{: .num_defn} ###### Definition 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. =--