What are `lexpr` and `ApplicationExpression` nltk?

What exactly does lexpr mean and what do the folloring r’/F x.x mean? Also what is Application Expression?

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()

Answer

See http://goo.gl/zog68k, nltk.sem.logic.Expression is:

“””This is the base abstract object for all logical expressions”””

There are many types of logical expressions implemented in nltk. See line 1124, the ApplicationExpression is:

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)”.

I’m not exactly an expert in formal logics but your code above is trying to declare a logical function variable 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)

For a crash course, see 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