タプルばー

tuple bar
http://d.hatena.ne.jp/nuc/20050905/p2

(f, g) (a, b) = (f a, g b)

となっているとうれしいなあ。と思ったわけですよ。これよく使うし、(\(as,bs,cs) -> ((x:as),bs,cs)) が ((x:),id,id) になるから。
でも、これを加えたラムダ計算が tuple の定義を変えてでも acceptable でないと、嫌です。
例えば、集合論の順序対が () = なのはなんとなく怖い。それは順序対の定義のせいではあるけれども、順序対の定義は深いところへ食い込んでいるからこれをしようと思うと公理までいじらなきゃいけなさそう。
(a, b) も所詮は一種の lambda なわけでこれを仮に cons a b とでもしておくと tuple というからには car と cdr がいる。
そうすると

find cons, car and cdr, such that for all a, b, f and g:
cons f g (cons a b) = cons (f a) (g b)
car (cons a b) = a
cdr (cons a b) = b

よく考えると、なんかいかにもできそう。

cons a b 0 = a
cons a b 1 = b
cons a b z = cons (a (car z)) (b (cdr z))

あ〜、ここで 1 をチャーチ数としていいのか? zとぶつかったらやだなあ。新たなアトムを持ち込みたくないけど。

cons a b 0 0 = a
cons a b 0 1 = b
cons a b z   = cons (a (car z)) (b (cdr z))

とすればいいか。一つにこだわることなくて。

バーで「SFバー」を思い出した。あまり関係ないし、前もリンクを貼った気がするけども、偉大な後輩の卒業文集を引っ張ってくる。
http://user.ecc.u-tokyo.ac.jp/~g441127/koukou.html