ベームの木

ラムダ計算の表示的意味論の研究において、Böhm木^{[ a ]}、Lévy-Longo木^{[ 1 ] [ 2 ] [ b ]}、およびBerarducci木^{[ 3 ]}は、（潜在的に無限の）木のような数学的対象であり、ある「意味のない」項の集合を除いて、項の「意味」を捉えます。

計算の意味を理解する簡単な方法は、それを有限個のステップからなる機械的な手順とみなし、完了すると結果が得られると考えることです。特に、ラムダ計算を書き換えシステムとみなすと、各ベータ還元ステップは書き換えステップであり、それ以上ベータ還元がなくなると項は正規形になります。したがって、チャーチの提案^{[ 4 ]}に素朴に従うと、項の意味はその正規形であり、正規形を持たない項は無意味であると言うことができます。例えば、${\displaystyle \mathbf {I} =\lambda xx}$そして${\displaystyle \mathbf {II} }$両方とも${\displaystyle \mathbf {I} }$これは、型付きラムダ計算など、ラムダ計算の任意の強力な正規化部分集合に対して機能します。

しかし、この単純な意味付けは、完全なラムダ計算には不十分である。${\displaystyle \mathbf {\Omega } =(\lambda x.xx)(\lambda x.xx)}$正規形はなく、同様に用語${\displaystyle \mathbf {X} =\lambda xx\mathbf {\Omega } }$正規形はありません。しかし、アプリケーションは${\displaystyle \mathbf {\オメガ } (\mathbf {KI} )}$、 どこ${\displaystyle \mathbf {K} }$標準ラムダ項を表す${\displaystyle \lambda x.\lambda yx}$はそれ自体に還元されるが、アプリケーションは${\displaystyle \mathbf {X} (\mathbf {KI} )}$通常のオーダー削減により、${\displaystyle \mathbf {I} }$したがって、意味があります。このように、すべての非正規化項が同等ではないことがわかります。${\displaystyle \mathbf {\オメガ } }$意味が薄い${\displaystyle \mathbf {X} }$適用するため${\displaystyle \mathbf {X} }$項に適用すると結果が生成されるが、${\displaystyle \mathbf {\オメガ } }$できません。

ボーム木は、無限大の項を含む無限ラムダ計算の文脈でも適用できます。この文脈では、項${\displaystyle \mathbf {NN} }$、 どこ${\displaystyle \mathbf {N} =\lambda x.\mathbf {I} (xx)}$、両方とも${\displaystyle \mathbf {I} (\mathbf {I} (\dots ))}$そして${\displaystyle \mathbf {\オメガ } }$そのため、正規化の合流にも問題がある。^{[ 5 ]}

一般的な構造は、一連のパラメータによって規定される。${\displaystyle U}$無意味な用語の、次の公理を満たすことが求められる: ^{[ 6 ] [ 7 ]}

• ルートアクティブ性: すべてのルートアクティブ項は${\displaystyle U}$用語${\displaystyle M}$すべての${\displaystyle M{\stackrel {*}{\to }}N}$redexが存在する${\displaystyle (\lambda xP)Q}$そのため${\displaystyle N{\stackrel {*}{\to }}(\lambda xP)Q}$。
• β還元下での閉鎖: すべての${\displaystyle M\in U}$、 もし${\displaystyle M{\stackrel {*}{\to }}N}$それから${\displaystyle N\in U}$。
• 代替による閉鎖: すべての${\displaystyle M\in U}$および代替${\displaystyle \sigma }$、${\displaystyle M\sigma \in U}$。
• 重複: すべての${\displaystyle \lambda xM\in U}$、${\displaystyle (\lambda xM)N\in U}$。
• 不可視性：すべての人にとって${\displaystyle M,N}$、 もし${\displaystyle N}$入手先は${\displaystyle M}$ペアごとに互いに素な部分項のセットを置き換えることによって${\displaystyle U}$その他の条件${\displaystyle U}$、 それから${\displaystyle M\in U}$かつその場合に限り${\displaystyle N\in U}$。
• β展開による閉鎖。すべてについて${\displaystyle N\in U}$、 もし${\displaystyle M{\stackrel {*}{\to }}N}$、 それから${\displaystyle M\in U}$定義によってはこれを省略しているものもありますが、これは有用です。^{[ 8 ]}

無意味な用語のセットは無限に存在するが、文献で最も一般的なものは次のとおりである。^{[ 9 ]}

• ヘッドのない項の集合の正規形
• 弱ヘッド正規形を持たない項の集合
• ルート活性項の集合、すなわち、最上位正規形またはルート正規形を持たない項の集合。ルート活性が前提とされているため、これは意味のない項の最小集合となる。

ご了承ください${\displaystyle \mathbf {\オメガ } }$ルート活性であるため${\displaystyle \mathbf {\オメガ } \in U}$あらゆる無意味な用語のセットに対して${\displaystyle U}$。

⊥ を持つ λ 項の集合 (λ⊥ 項と略記) は、文法によって帰納的に定義される。${\displaystyle M=\bot \mid x\mid (\lambda xM)\mid (MM)}$これは、標準的な無限ラムダ計算に以下の項を加えたものに相当する。${\displaystyle \bot }$この集合に対するベータ縮小は標準的な方法で定義されます。意味のない用語の集合が与えられた場合${\displaystyle U}$また、底辺への還元も定義します。${\displaystyle M[\bot \mapsto \mathbf {\Omega } ]\in U}$そして${\displaystyle M\neq \bot }$、 それから${\displaystyle M\to \bot }$λ⊥項は、これら2つの規則を持つ書き換えシステムとして考えられます。無意味な項の定義のおかげで、この書き換えシステムは合流的で正規化されています。^{[ 7 ]}

項に対するベーム型「ツリー」は、このシステムにおける項の正規形として得られる可能性があり、項が無限に拡大する場合は、おそらく「極限」の意味で無限となる。