lexpr は正確には何を意味し、次の r'/F xx は何を意味しますか? また、アプリケーション式とは何ですか?
from nltk.sem.logic import *
lexpr = Expression.fromstring
zero = lexpr(r'\F x.x')
one = lexpr(r'\F x.F(x)')
two = lexpr(r'\F x.F(F(x))')
three = lexpr(r'\F x.F(F(F(x)))')
four = lexpr(r'\F x.F(F(F(F(x))))')
succ = lexpr(r'\N F x.F(N(F,x))')
plus = lexpr(r'\M N F x.M(F,N(F,x))')
mult = lexpr(r'\M N F.M(N(F))')
pred = lexpr(r'\N F x.(N(\G H.H(G(F)))(\u.x)(\u.u))')
v1 = ApplicationExpression(succ, zero).simplify()
http://goo.gl/zog68kを参照してくださいnltk.sem.logic.Expression。
"""これはすべての論理式の基本抽象オブジェクトです"""
には多くの種類の論理式が実装されていnltkます。1124 行を参照してくださいApplicationExpression。
このクラスは、関連する 2 つのタイプの論理式を表すために使用されます。
1 つ目は、「P(x,y)」などの述語式です。述語式は、述語としての
FunctionVariableExpressionorConstantExpressionと、引数としての式のリストで構成されます。2 つ目は、"(\x.dog(x))(fido)" のように、ある式を別の式に適用したものです。
述語式がアプリケーション式として扱われる理由は、式の変数式述語が LambdaExpression などの別の式に置き換えられる可能性があるためです。これは、述語が引数に適用されると考えられる必要があることを意味します。
論理式リーダーは、常にアプリケーション式の引数をカリー化します。したがって、「\x y.see(x,y)(john,mary)」は、内部的には「((\x y.(see(x))(y))(john))(mary)」と表現されます。アプリケーションには常に 1 つの引数しかないため、これにより内部構造が簡素化されます。
str() メソッドは通常、カリー化された形式のアプリケーション式を出力します。1 つの例外は、アプリケーション式が実際に述語式である場合 (つまり、基になる関数が である場合
AbstractVariableExpression) です。これは、上記の例が "(\x y.see(x,y)(john))(mary)" として返されることを意味します。
私は形式論理の専門家ではありませんが、上記のコードは論理関数変数 x を宣言しようとしています。
>>> from nltk.sem.logic import *
>>> lexpr = Expression.fromstring
>>> zero = lexpr(r'\F x.x')
>>> succ = lexpr(r'\N F x.F(N(F,x))')
>>> v1 = ApplicationExpression(succ, zero).simplify()
>>> v1
<LambdaExpression \F x.F(x)>
>>> print v1
\F x.F(x)
短期集中コースについては、 http://theory.stanford.edu/~arbrad/slides/cs156/lec2-4.pdf を参照してください。ラムダ式の nltk 短期集中コースについては、 http: //www.cs.utsa.edu/ を参照してください。 ~bylander/cs5233/nltk-intro.pdf
あなたは非常に複雑なツールキットのごく一部を見ています。以下の Web でのちょっとした調査から、いくつかの背景を説明しようとします。または、必要に応じて「直接的な回答」セクションにスキップすることもできます。あなたが引用した特定の部分についてあなたの質問に答えようとしますが、私は哲学的論理または自然言語処理の専門家ではありません. それについて読めば読むほど、私が知らないように見えますが、役立つと思われる参考文献をたくさん含めました。
あなたが投稿したコードは、python (NLTK) 用の自然言語ツールキットのロジック モジュールの回帰テストのサブシリーズです。このツールキットは、ツールの作成者によって書かれたように見える、かなりアクセスしやすい学術論文 (こちら) で説明されています。ツールキットの動機とロジック モジュールの作成について説明しています。一言で言えば、自然言語の解釈を自動化するのに役立ちます。
あなたが投稿したコードは、いくつかの論理形式を定義しています (私がリンクした論文で言及されている LF)。LF は、ラムダ演算子 (つまり、一次ラムダ計算)と組み合わせた一次述語論理のステートメントをカバーします。ここでは、一次述語ロジックを完全に説明するつもりはありません。ここにラムダ計算に関するチュートリアルがあります。
このコードは、ハウツー ページの一連の回帰テスト(つまり、ツールボックスが単純な既知のサンプル テストで正しく動作することのデモンストレーション) に由来し、ツールボックスを使用して単純な算術演算を実行する方法を示しています。これらは、nltk ツールキットのラムダ計算 (ウィキペディア リンク) による算術へのこのアプローチを正確にエンコードしたものです。
最初の 4 つは、ラムダ計算 ( Church Encoding ) の最初の 4 つの数値です。次の 4 つは算術演算子です - succ(後継)、plus(加算)、mult(乗算)、pred(除算)。これらに対応するテストはまだありません。そのため、現時点では単純に LF の数があり、その後にこれらの LF の 2 つ (succとzero) を組み合わせて を得る、ラムダ計算の一例v1。あなたが適用 succしたようzeroに、結果は 1 でなければなりません - そしてそれはハウツーページで彼らがテストするものです - すなわちv1 == one評価すべきTrueです。
投稿したコードの要素を 1 つずつ見ていきましょう。
lexpr論理式 EXPRession を生成する関数です - as のエイリアスExpression.fromstringですlexpr = Expression.fromstring
文字列引数を取ります。文字列の前の r は、Python に生の文字列リテラルとして解釈するように指示します。この質問の目的のために-つまり、\シンボルをエスケープする必要はありません
文字列内に\は、ラムダ演算子があります。
Fxラムダ計算で関数と束縛変数を表す
or ドット演算子は.、バインドされた関数を式/抽象化の本体から分離します
つまり、質問で引用した文字列を取得するには：
r'/F x.x'
ゼロの教会符号化です。教会のエンコーディングはかなり抽象的で、理解するのが難しいです。このチュートリアルが役立つかもしれません- 私はそれを理解し始めていると思います...残念ながら、あなたが選択した例はゼロであり、私が解決できることから、これは定義であり、派生できるものではありません。意味のある意味で「0に評価」することはできません。 これは私が見つけた最も簡単な説明です。私はその厳密性/正確性についてコメントする立場にありません。
チャーチ数字は引数を 1 つ取る手順であり、その引数自体も引数を 1 つ取る別の手順です。プロシージャ zero は、その入力プロシージャを 0 回適用するプロシージャを返すことにより、整数 0 を表します。
最後に、ApplicationExpressionは 1 つの式を取得し、それを別の式に適用します。この場合はsucc(後続) を に適用しzeroます。これは、適切に、ラムダ計算のアプリケーションと呼ばれます
編集：
それをすべて書いた後、nltk サイトに隠された本を見つけました -第 10 章は特にこの質問に当てはまり、このセクションではラムダ計算について説明しています。