tozima's blog

主に自分のための、論文の読書記録

型無しλ計算の big-step semantics と game semantics

　　　　次のようなツイートを見かけたので、私なりの回答を。

　　　　「計算が止まらない」には少なくとも二種類、

(\lambda x. x\,x) (\lambda x. x\,x) \longrightarrow (\lambda x. x\,x) (\lambda x. x\,x)

のように無意味な計算が延々続くものと、

\lambda f. Y\,f \longrightarrow \lambda f. f (Y\,f) \longrightarrow \lambda f. f (f (Y\,f)) \longrightarrow \dots \longrightarrow \lambda f. f (f (f (f \dots))))

のように意味のある計算が続いた結果として無限サイズの値を返すものがあって、これらは区別されます。通常の型無しλ計算の big-step semantics では後者の評価は「停止する」と考えます。

　　　　Big-step semantics は項 Mと値 Vの関係 M \Downarrow Vを与えるものですから、はじめに「値はなにか」ということを考える必要があります。型無しλ計算では、値をλ抽象 \lam x. Mとするのが通例で、住井先生の以下のツイートもこの設定での話であろうと思います。

 

値をすべてのλ抽象とした場合、「評価が停止しない」項はBoehm木も \bot であり、Boehm木で考えても一点につぶれています（また game semantics でも一点に潰れます）。またBoehm木が \botでないなら、遅くとも head variable が決まるときには「評価が停止」しています。ちなみに逆は成り立たなくて、Boehm木は \bot だが「評価が停止する」項が存在します。例えば M = \lambda f. \lambda x. fとして、 N = M (Y\,M)を考えます。すると、

N = M (Y\,M) \longrightarrow \lambda x. Y\,M

ですので評価は停止します。しかしながら、

\lambda x. Y\,M \longrightarrow \lambda x. M (Y\,M) = \lambda x. N

であることを踏まえると、

N \longrightarrow^* \lambda x. N \longrightarrow^* \lambda x. \lambda y. N \longrightarrow^* \dots

となり NのBoehm木は \botです。

 　　　　それでは値をBoehm木とするような big-step semantics は考えられるかというと、困難があるように思います。できるのなら co-inductive なルールに基づく評価規則になるのだろうと思いますが、適用の規則が難しそうです。それなら game semantics でいいじゃないか、と思ってしまいます。
　　　　最後に small-step semantics との関係について。まず、small-step semantics と Boehm thoery は異なります。βη同値な項は同じBoehm木を持ちますが、同じBoehm木を持つβη同値ではない項が知られています。*1直観的には、βη同値性は有限ステップの簡約による等しさで、Boehm木の等しさは無限ステップの簡約による等しさなので、後者の方が各同値類が大きいということになるかと思います。

 

*1:Wikipediaの不動点演算子か何かの項に例があったと思います。βη同値ではないが、同じBoehm木はλf. f (f (f ...) )を持つ項が挙げられていたはずです。