λ代数、万能対象

自己適用の分析のために、確か適用構造だか適用代数だかという概念があったと思う。適用に相当する二項演算・があって、それがナニガシかの公理を満たすようなものだったと思うのだけど、あんまり憶えてない。

とりあえず、横内さんの『プログラム意味論』を探した。適用構造はなかったが、似たような話でλ代数があった。少しアレンジして述べる。

まず、λ演繹系（横内本にはない）(V, L, |-)を次のように定義する。

1. 変数の集合V
2. Vから構文的な適用とラムダ抽象から生成された式（項）の集合L
3. 2つの式M, Nから作られる同値性のjudgement M = N （単なる構文）
4. M = N を導出するための書き換え／推論規則と、演繹（導出）可能性判を示す |-。

Sがλ演繹系なら、|- M = N という主張が意味を持つ。λ演繹系の具体例は形無しのラムダ計算から作れる。もっとも、書き換え／推論規則の具体的な構成は難しいが。

λ演繹系S上のラムダ代数は、二項演算・を備えた集合X、環境Env=Map(V, X)、意味写像[(-:-)] : L×Env→X からなる系で：

1. [(x:α)] = α(x)
2. FreeVars(M)上でαとβが一致するなら、[(M:α)] = [(M:β)]
3. [(M N :α)] = [(M :α)]・[(N :α)]
4. [(λx.M :α)]・d = [(M :α[x:=d)]
5. |- M = N ⇒ ∀α.([(M : α)] = [(N : α)])

要するに、形無しのもっとも単純なλ演繹系に対する都合のよいモデルのことだ。ただし、λモデルというより広い概念はまた別にあるようだ。

---

ついでに、反射的対象と万能対象についても。

Vが反射的対象とは、ベキ[V, V]がVに埋め込めること。ここで、埋め込めるは単なる単射じゃなくてEPペアの存在を仮定する。別な言い方をすると、i:[V, V]→V に対してレトラクト（または射影）rがあって、i;r = id が成立している。

万能対象の万能はおそらくuniversalだろう。「反射的対象とスノーグローブな世界」で「普遍」は使えない、と言ったが、どうやら使ってしまっているようだ。Uが万能だとは：

1. 任意の対象Aに対して、埋め込み A→U が存在する。ここで埋め込みはEPペア。
2. h:U→Uがベキ等ならば、h = r_A;i_A となるEPペアが存在する。

万能対象は任意の対象を内包するだけでなく、ベキ等射がEPペアで表現できるという条件が付く。つまり、外の圏の対象類全体を万能対象のベキ等射として埋め込めることになる。そう言えば、「全然知らないことが山盛り載っていた」のカロウビ展開圏が、ベキ等射を対象とみなす構成だったと思う。