什么是 `lexpr` 和 `ApplicationExpression` nltk?

What are `lexpr` and `ApplicationExpression` nltk?

lexpr 到底是什么意思,后面的 r'/F x.x 是什么意思?还有什么是应用程序表达式?

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/zog68knltk.sem.logic.Expression是:

"""This is the base abstract object for all logical expressions"""

nltk中实现了多种类型的逻辑表达式。参见第 1124 行,ApplicationExpression 是:

This class is used to represent two related types of logical expressions.

The first is a Predicate Expression, such as "P(x,y)". A predicate expression is comprised of a FunctionVariableExpression or ConstantExpression as the predicate and a list of Expressions as the arguments.

The second is a an application of one expression to another, such as "(\x.dog(x))(fido)".

The reason Predicate Expressions are treated as Application Expressions is that the Variable Expression predicate of the expression may be replaced with another Expression, such as a LambdaExpression, which would mean that the Predicate should be thought of as being applied to the arguments.

The logical expression reader will always curry arguments in a application expression. So, "\x y.see(x,y)(john,mary)" will be represented internally as "((\x y.(see(x))(y))(john))(mary)". This simplifies the internals since there will always be exactly one argument in an application.

The str() method will usually print the curried forms of application expressions. The one exception is when the the application expression is really a predicate expression (ie, underlying function is an AbstractVariableExpression). This means that the example from above will be returned as "(\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 and a nltk crash course to lambda expressions, see http://www.cs.utsa.edu/~bylander/cs5233/nltk-intro.pdf

您看到的是相当复杂的工具包中的一小部分。我尝试通过在下面的网络上进行一些研究来提供一些背景知识。或者,如果您愿意,可以直接跳到 "direct answers" 部分。我会尝试根据您引用的特定部分回答您的问题,但我不是哲学逻辑或自然语言处理方面的专家。我读得越多,似乎知道的就越少,但我已经包含了很多有用的参考资料。

工具描述/原理/介绍

您发布的代码是 python (NLTK) 自然语言工具包逻辑模块回归测试的子系列。该工具包在 fairly accessible academic paper here 中进行了描述,似乎是由该工具的作者编写的。它描述了工具包和编写逻辑模块的动机 - 简而言之,以帮助自动解释自然语言。

您发布的代码定义了许多逻辑形式(我链接的论文中提到的 LF)。 LF 覆盖 First order predicate logic, combined with the lambda operator (i.e. first order lambda calculus). I will not attempt to completely describe First order predicate logic here. There's a tutorial on lambda calculus here.

中的语句

代码来自nltk工具包中的一组regression tests (i.e. demonstrations that the toolbox works correctly on simple, known exmample tests) on the howto page, demonstrating how the toolbox can be demonstrated by using it to do simple arithmetic operations. They are an exact encoding of this approach to arithmetic via lambda calculus (Wikipedia link)

前四位是 lambda 演算中的前四位数字 (Church Encoding)。接下来的四个是算术运算符 - succ(后继),plus(加法),mult(乘法)和 pred(除法),你没有得到测试跟着这些,所以目前,你只是有一些 LF,然后是一个 Lambda 演算的例子,结合这些 LF 中的两个(succzero)得到 v1.因为你有 applied succzero,结果应该是一个 - 这就是他们在 howto 页面上测试的 - 即 v1 == one应该评估 True.

直接回答python位

让我们一一浏览您发布的代码的元素。

lexpr 是生成逻辑表达式的函数 - 它是 Expression.fromstring 的别名,如 lexpr = Expression.fromstring

它接受一个字符串参数。字符串前的 r 告诉 python 将其解释为 原始字符串文字 。出于这个问题的目的 - 这意味着我们不必转义 \ 符号

在字符串中,\ 是 lambda 运算符。

F 表示函数,x lambda 演算中的绑定变量

. 或点运算符将绑定函数与表达式/抽象的主体分开

所以 - 取你在问题中引用的字符串:

r'/F x.x'

是零的Church Encoding。 Church 编码非常抽象,很难理解。这个 教程可能会有所帮助 - 我想我开始明白了......不幸的是你选择的例子是零,根据我的计算,这是一个 定义,而不是你可以推导出来的东西。它不能是任何有意义的 "evaluated to 0"。 这是我找到的最简单的解释。我无法评论它的严谨性/正确性。

A Church numeral is a procedure that takes one argument, and that argument is itself another procedure that also takes one argument. The procedure zero represents the integer 0 by returning a procedure that applies its input procedure zero times

最后,ApplicationExpression 采用一个表达式,将其应用 到另一个,在本例中,将 succ(后继)应用到 zero.这在 lambda 演算

中被恰当地称为 应用程序

编辑:

写了所有这些,然后发现 book hidden on the nltk site - Chapter 10 is particularly applicable to this question, with this section 描述 lambda 演算。