What are `lexpr` and `ApplicationExpression` nltk?

Question

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 1

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

Answer 2

You are looking at a small part of quite a complicted toolkit. I try to give some background from a bit of researching on the web below. Or you can just skip to the "direct answers" section if you like. I'll try to answer your question on the specific part you quote, but I am not an expert on either philosophical logic or natural language processing. The more I read about it, the less I seem to know, but I've included a load of hopefully useful references.

Description of tool / principles/ introduction

The code you've posted is a sub-series of the regression tests for the logic module of the Natural Language toolkit for python (NLTK). This toolkit is described in a fairly accessible academic paper here, seemingly written by the authors of the tool. It describes the motivation for the toolkit and writing the logic module - in a nutshell to help automate interpretation of natural language.

The code you've posted defines a number of logical forms (LFs as they are referred to in the paper I linked). LFs cover statements in 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.

The code comes from a set of 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) in the nltk toolkit.

The first four are the first four numbers in lambda calculus (Church Encoding). The next four are arithmetic operators - succ (successor), plus (addition), mult (multiplication) and pred (division), You have not got the tests that go along with these, so at the moment, you simply have a number of LFs, followed by one example of Lambda calculus, combining two of these LFs (succ and zero) to get v1. as you have applied succ to zero, the result should be one - and that is what they test for on the howto page - i.e. v1 == one should evaluate True.

Direct answer to python bits

Lets go through the elements of the code you've posted one by one.

lexpr is the function that generates Logical EXPRessions - it is an alias for Expression.fromstring as lexpr = Expression.fromstring

It takes a string argument. The r before the string tells python to interpret it as a raw string literal. For the purposes of this question - that means that we don't have to escape the \ symbol

Within the Strings, \ is the lambda operator.

F denotes a function and x a bound variable in lambda calculus

The . or dot operator separates the bound function from the body of the expression / abstraction

So - to take the string you quote in the question:

r'/F x.x'

It is the Church Encoding of zero. Church encoding is pretty abstract and hard to get your head round. This tutorial might help - I think I'm starting to get it... Unfortunately the example you've chosen is zero and from what I can work out, this is a definition, rather than something you can derive. It can't be "evaluated to 0" in any meaningful sense. This is the simplest explanation I've found. I'm not in a position to comment on its rigour / correctness.

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

Finally, the ApplicationExpression is taking one expression and applying it to the other, in this case applying succ (succesor) to zero. This is, aptly, called an application in lambda calculus

EDIT:

Wrote all that and then found a book hidden on the nltk site - Chapter 10 is particularly applicable to this question, with this section describing lambda calculus.