ラムダ計算の重箱の隅(?)：タプルと成分

やっぱり多圏の議論をしないとどうにもならない、と感じる。ラムダ計算は、「タプルを出さないのが粋」みたいな風潮にもウンザリ。

タプルを扱うなら、項レベルでペア構文 (E, F) は必要だ。これを、カンマが二項演算子と解釈する。ただし、カンマは左結合的で適用よりは結合度（優先順位）が弱いとする。

• x, y, z は (x, y), z
• f x, y は (f x), y
• f (x, y) はそのまんま

次に、.1と.2という多相なドット演算子を導入して、

• (E, F).1 → E
• (E, F).2 → F

と書き換え規則を導入する。射影（を表すラムダ項）は次のように定義できる。

• prj1 := λz:A×B.z.1
• prj2 := λz:A×B.z.2

prj1 (x, y) = x は次の書き換えで示せる。

   prj1 (x, y)
→ (λz:A×B.z.1)(x, y)
→ (x, y).1
→ x

それはいいのだが、長いタプルtに対する、t.3, t.4 とかをどう定義するか？は問題だ。

.1, .2は組み込み演算子として、.3, .4とかの演算子を定義したときの自然数 1, 2, 3, 4, ... は何なんだ？つう話がある。ラムダ項の構文内部に自然数を最初から入れるか、または定義するのか、それとも、成分番号の自然数はあくまでラムダ項の外の演算子構文の一部なのか？ 項と項に対する略記の境界線が問題になる。

ラムダ項の全体をTermとして、自然数は項の外にあるとすると、Term×N→Term を、ラムダ項の構造と自然数を合わせた帰納的構造のなかで帰納法を使って定義することになる。

Nat⊆Term, NatNとすれば、Term×Nat→Termでタプルの射影（成分取り出し）を定義することになる。

どっちの方法であれ、項書換えがモデルである直積として振舞っているか、つまり、タプルの射影に関する構文的操作が、デカルト圏のデカルトモノイド積のモデルになっているのか、を検証しなくてはならない。

重箱の隅でもないな、これは。