Logic & Lambda Calculus

  
>>> from nltk.sem import *

Test for equality under alpha-conversion.

  
>>> lp = LogicParser()
>>> e1 = lp.parse('exists x.P(x)')
>>> print e1
exists x.P(x)
>>> e2 = e1.alpha_convert(Variable('z'))
>>> print e2
exists z.P(z)
>>> e1 == e2
True
  
>>> l = lp.parse(r'(\X.\X.X(X)(1))').simplify()
>>> id = lp.parse(r'\X.X(X)')
>>> l == id
True

Test numerals

  
>>> zero = lp.parse(r'\F x.x')
>>> one = lp.parse(r'\F x.F(x)')
>>> two = lp.parse(r'\F x.F(F(x))')
>>> three = lp.parse(r'\F x.F(F(F(x)))')
>>> four = lp.parse(r'\F x.F(F(F(F(x))))')
>>> succ = lp.parse(r'\N F x.F(N(F,x))')
>>> plus = lp.parse(r'\M N F x.M(F,N(F,x))')
>>> mult = lp.parse(r'\M N F.M(N(F))')
>>> pred = lp.parse(r'\N F x.(N(\G H.H(G(F)))(\u.x)(\u.u))')
>>> v1 = ApplicationExpression(succ, zero).simplify()
>>> v1 == one
True
>>> v2 = ApplicationExpression(succ, v1).simplify()
>>> v2 == two
True
>>> v3 = ApplicationExpression(ApplicationExpression(plus, v1), v2).simplify()
>>> v3 == three
True
>>> v4 = ApplicationExpression(ApplicationExpression(mult, v2), v2).simplify()
>>> v4 == four
True
>>> v5 = ApplicationExpression(pred, ApplicationExpression(pred, v4)).simplify()
>>> v5 == two
True

Overloaded operators also exist for convenience

  
>>> print succ(zero).simplify() == one
True
>>> print plus(one,two).simplify() == three
True
>>> print mult(two,two).simplify() == four
True
>>> print pred(pred(four)).simplify() == two
True
  
>>> john = lp.parse(r'john')
>>> man = lp.parse(r'\x.man(x)')
>>> walk = lp.parse(r'\x.walk(x)')
>>> man(john).simplify()
<ApplicationExpression man(john)>
>>> print -walk(john).simplify()
-walk(john)
>>> print (man(john) & walk(john)).simplify()
(man(john) & walk(john))
>>> print (man(john) | walk(john)).simplify()
(man(john) | walk(john))
>>> print (man(john) > walk(john)).simplify()
(man(john) -> walk(john))
>>> print (man(john) < walk(john)).simplify()
(man(john) <-> walk(john))

Python's built-in lambda operator can also be used with Expressions

  
>>> john = VariableExpression(Variable('john'))
>>> run_var = VariableExpression(Variable('run'))
>>> run = lambda x: run_var(x)
>>> run(john)
<ApplicationExpression run(john)>

1
   betaConversionTestSuite.pl

From B&B's Representation and Inference for Natural Language.

  
>>> x1 = lp.parse(r'\P.P(mia)(\x.walk(x))').simplify()
>>> x2 = lp.parse(r'walk(mia)').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'exists x.(man(x) & ((\P.exists x.(woman(x) & P(x)))(\y.love(x,y))))').simplify()
>>> x2 = lp.parse(r'exists x.(man(x) & exists y.(woman(y) & love(x,y)))').simplify()
>>> x1 == x2
True
>>> x1 = lp.parse(r'\a.sleep(a)(mia)').simplify()
>>> x2 = lp.parse(r'sleep(mia)').simplify()
>>> x1 == x2
True
>>> x1 = lp.parse(r'\a.\b.like(b,a)(mia)').simplify()
>>> x2 = lp.parse(r'\b.like(b,mia)').simplify()
>>> x1 == x2
True
>>> x1 = lp.parse(r'\a.(\b.like(b,a)(vincent))').simplify()
>>> x2 = lp.parse(r'\a.like(vincent,a)').simplify()
>>> x1 == x2
True
>>> x1 = lp.parse(r'\a.((\b.like(b,a)(vincent)) & sleep(a))').simplify()
>>> x2 = lp.parse(r'\a.(like(vincent,a) & sleep(a))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'(\a.\b.like(b,a)(mia)(vincent))').simplify()
>>> x2 = lp.parse(r'like(vincent,mia)').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'P((\a.sleep(a)(vincent)))').simplify()
>>> x2 = lp.parse(r'P(sleep(vincent))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'\A.A((\b.sleep(b)(vincent)))').simplify()
>>> x2 = lp.parse(r'\A.A(sleep(vincent))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'\A.A(sleep(vincent))').simplify()
>>> x2 = lp.parse(r'\A.A(sleep(vincent))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'(\A.A(vincent)(\b.sleep(b)))').simplify()
>>> x2 = lp.parse(r'sleep(vincent)').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'\A.believe(mia,A(vincent))(\b.sleep(b))').simplify()
>>> x2 = lp.parse(r'believe(mia,sleep(vincent))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'(\A.(A(vincent) & A(mia)))(\b.sleep(b))').simplify()
>>> x2 = lp.parse(r'(sleep(vincent) & sleep(mia))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'\A.\B.(\C.C(A(vincent))(\d.probably(d)) & (\C.C(B(mia))(\d.improbably(d))))(\e.walk(e))(\e.talk(e))').simplify()
>>> x2 = lp.parse(r'(probably(walk(vincent)) & improbably(talk(mia)))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'(\a.\b.(\C.C(a,b)(\d.\e.love(d,e))))(jules)(mia)').simplify()
>>> x2 = lp.parse(r'love(jules,mia)').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'(\A.\B.exists c.(A(c) & B(c)))(\d.boxer(d),\d.sleep(d))').simplify()
>>> x2 = lp.parse(r'exists c.(boxer(c) & sleep(c))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'\a.Z(a)(\c.\a.like(a,c))').simplify()
>>> x2 = lp.parse(r'Z(\c.\a.like(a,c))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'\A.\b.A(b)(\c.\b.like(b,c))').simplify()
>>> x2 = lp.parse(r'\b.(\c.\b.like(b,c)(b))').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'(\a.\b.(\C.C(a,b)(\b.\a.loves(b,a))))(jules)(mia)').simplify()
>>> x2 = lp.parse(r'loves(jules,mia)').simplify()
>>> x1 == x2
True
  
>>> x1 = lp.parse(r'(\A.\b.(exists b.A(b) & A(b)))(\c.boxer(c))(vincent)').simplify()
>>> x2 = lp.parse(r'((exists b.boxer(b)) & boxer(vincent))').simplify()
>>> x1 == x2
True

Test Parser

  
>>> print lp.parse(r'john')
john
>>> print lp.parse(r'x')
x
>>> print lp.parse(r'-man(x)')
-man(x)
>>> print lp.parse(r'--man(x)')
--man(x)
>>> print lp.parse(r'(man(x))')
man(x)
>>> print lp.parse(r'((man(x)))')
man(x)
>>> print lp.parse(r'man(x) <-> tall(x)')
(man(x) <-> tall(x))
>>> print lp.parse(r'(man(x) <-> tall(x))')
(man(x) <-> tall(x))
>>> print lp.parse(r'(man(x) & tall(x) & walks(x))')
(man(x) & (tall(x) & walks(x)))
>>> print lp.parse(r'((man(x) & tall(x)) & walks(x))')
((man(x) & tall(x)) & walks(x))
>>> print lp.parse(r'(man(x) & (tall(x) & walks(x)))')
(man(x) & (tall(x) & walks(x)))
>>> print lp.parse(r'exists x.man(x)')
exists x.man(x)
>>> print lp.parse(r'exists x.(man(x) & tall(x))')
exists x.(man(x) & tall(x))
>>> lp.parse(r'-P(x) & Q(x)') == lp.parse(r'(-P(x)) & Q(x)')
True
>>> print lp.parse(r'\x.man(x)')
\x.man(x)
>>> print lp.parse(r'\x.man(x)(john)')
\x.man(x)(john)
>>> print lp.parse(r'\x.man(x)(john) & tall(x)')
(\x.man(x)(john) & tall(x))
>>> print lp.parse(r'\x.\y.sees(x,y)')
\x.\y.sees(x,y)
>>> print lp.parse(r'\x  y.sees(x,y)')
\x.\y.sees(x,y)
>>> print lp.parse(r'\x.\y.sees(x,y)(a)')
(\x.\y.sees(x,y))(a)
>>> print lp.parse(r'\x  y.sees(x,y)(a)')
(\x.\y.sees(x,y))(a)
>>> print lp.parse(r'\x.\y.sees(x,y)(a)(b)')
((\x.\y.sees(x,y))(a))(b)
>>> print lp.parse(r'\x  y.sees(x,y)(a)(b)')
((\x.\y.sees(x,y))(a))(b)
>>> print lp.parse(r'\x.\y.sees(x,y)(a,b)')
((\x.\y.sees(x,y))(a))(b)
>>> print lp.parse(r'\x  y.sees(x,y)(a,b)')
((\x.\y.sees(x,y))(a))(b)
>>> print lp.parse(r'((\x.\y.sees(x,y))(a))(b)')
((\x.\y.sees(x,y))(a))(b)
>>> print lp.parse(r'P(x)(y)(z)')
P(x,y,z)
>>> print lp.parse(r'P(Q)')
P(Q)
>>> print lp.parse(r'P(Q(x))')
P(Q(x))
>>> print lp.parse(r'(\x.exists y.walks(x,y))(x)')
(\x.exists y.walks(x,y))(x)
>>> print lp.parse(r'exists x.(x = john)')
exists x.(x = john)
>>> print lp.parse(r'((\P.\Q.exists x.(P(x) & Q(x)))(\x.dog(x)))(\x.bark(x))')
((\P.\Q.exists x.(P(x) & Q(x)))(\x.dog(x)))(\x.bark(x))
>>> a = lp.parse(r'exists c.exists b.A(b,c) & A(b,c)')
>>> b = lp.parse(r'(exists c.(exists b.A(b,c))) & A(b,c)')
>>> print a == b
True
>>> a = lp.parse(r'exists c.(exists b.A(b,c) & A(b,c))')
>>> b = lp.parse(r'exists c.((exists b.A(b,c)) & A(b,c))')
>>> print a == b
True
>>> lp.parse(r'exists x.x = y') == lp.parse(r'exists x.(x = y)')
True
>>> print lp.parse(r'A != B')
-(A = B)

Simplify

  
>>> print lp.parse(r'\x.man(x)(john)').simplify()
man(john)
>>> print lp.parse(r'\x.((man(x)))(john)').simplify()
man(john)
>>> print lp.parse(r'\x.\y.sees(x,y)(john, mary)').simplify()
sees(john,mary)
>>> print lp.parse(r'\x  y.sees(x,y)(john, mary)').simplify()
sees(john,mary)
>>> print lp.parse(r'\x.\y.sees(x,y)(john)(mary)').simplify()
sees(john,mary)
>>> print lp.parse(r'\x  y.sees(x,y)(john)(mary)').simplify()
sees(john,mary)
>>> print lp.parse(r'\x.\y.sees(x,y)(john)').simplify()
\y.sees(john,y)
>>> print lp.parse(r'\x  y.sees(x,y)(john)').simplify()
\y.sees(john,y)
>>> print lp.parse(r'(\x.\y.sees(x,y)(john))(mary)').simplify()
sees(john,mary)
>>> print lp.parse(r'(\x  y.sees(x,y)(john))(mary)').simplify()
sees(john,mary)
>>> print lp.parse(r'exists x.(man(x) & (\x.exists y.walks(x,y))(x))').simplify()
exists x.(man(x) & exists y.walks(x,y))
>>> e1 = lp.parse(r'exists x.(man(x) & (\x.exists y.walks(x,y))(y))').simplify()
>>> e2 = lp.parse(r'exists x.(man(x) & exists z1.walks(y,z1))')
>>> e1 == e2
True
>>> print lp.parse(r'(\P Q.exists x.(P(x) & Q(x)))(\x.dog(x))').simplify()
\Q.exists x.(dog(x) & Q(x))
>>> print lp.parse(r'((\P.\Q.exists x.(P(x) & Q(x)))(\x.dog(x)))(\x.bark(x))').simplify()
exists x.(dog(x) & bark(x))
>>> print lp.parse(r'\P.(P(x)(y))(\a b.Q(a,b))').simplify()
Q(x,y)

Replace

  
>>> a = lp.parse(r'a')
>>> x = lp.parse(r'x')
>>> y = lp.parse(r'y')
>>> z = lp.parse(r'z')
  
>>> print lp.parse(r'man(x)').replace(x.variable, a, False)
man(a)
>>> print lp.parse(r'(man(x) & tall(x))').replace(x.variable, a, False)
(man(a) & tall(a))
>>> print lp.parse(r'exists x.man(x)').replace(x.variable, a, False)
exists x.man(x)
>>> print lp.parse(r'exists x.man(x)').replace(x.variable, a, True)
exists a.man(a)
>>> print lp.parse(r'exists x.give(x,y,z)').replace(y.variable, a, False)
exists x.give(x,a,z)
>>> print lp.parse(r'exists x.give(x,y,z)').replace(y.variable, a, True)
exists x.give(x,a,z)
>>> e1 = lp.parse(r'exists x.give(x,y,z)').replace(y.variable, x, False)
>>> e2 = lp.parse(r'exists z1.give(z1,x,z)')
>>> e1 == e2
True
>>> e1 = lp.parse(r'exists x.give(x,y,z)').replace(y.variable, x, True)
>>> e2 = lp.parse(r'exists z1.give(z1,x,z)')
>>> e1 == e2
True
>>> print lp.parse(r'\x y z.give(x,y,z)').replace(y.variable, a, False)
\x.\y.\z.give(x,y,z)
>>> print lp.parse(r'\x y z.give(x,y,z)').replace(y.variable, a, True)
\x.\a.\z.give(x,a,z)
>>> print lp.parse(r'\x.\y.give(x,y,z)').replace(z.variable, a, False)
\x.\y.give(x,y,a)
>>> print lp.parse(r'\x.\y.give(x,y,z)').replace(z.variable, a, True)
\x.\y.give(x,y,a)
>>> e1 = lp.parse(r'\x.\y.give(x,y,z)').replace(z.variable, x, False)
>>> e2 = lp.parse(r'\z1.\y.give(z1,y,x)')
>>> e1 == e2
True
>>> e1 = lp.parse(r'\x.\y.give(x,y,z)').replace(z.variable, x, True)
>>> e2 = lp.parse(r'\z1.\y.give(z1,y,x)')
>>> e1 == e2
True
>>> print lp.parse(r'\x.give(x,y,z)').replace(z.variable, y, False)
\x.give(x,y,y)
>>> print lp.parse(r'\x.give(x,y,z)').replace(z.variable, y, True)
\x.give(x,y,y)

Variables / Free

  
>>> print lp.parse(r'walk(john)').variables()
set([Variable('john'), Variable('walk')])
>>> print lp.parse(r'walk(x)').variables()
set([Variable('x'), Variable('walk')])
>>> print lp.parse(r'see(john,mary)').variables()
set([Variable('see'), Variable('john'), Variable('mary')])
>>> print lp.parse(r'exists x.walk(x)').variables()
set([Variable('walk')])
>>> print lp.parse(r'\x.see(john,x)').variables()
set([Variable('see'), Variable('john')])
>>> print lp.parse(r'\x.see(john,x)(mary)').variables()
set([Variable('see'), Variable('john'), Variable('mary')])
  
>>> print lp.parse(r'walk(john)').free()
set([])
>>> print lp.parse(r'walk(x)').free()
set([Variable('x')])
>>> print lp.parse(r'see(john,mary)').free()
set([])
>>> print lp.parse(r'exists x.walk(x)').free()
set([])
>>> print lp.parse(r'\x.see(john,x)').free()
set([])
>>> print lp.parse(r'\x.see(john,x)(mary)').free()
set([])
  
>>> print lp.parse(r'walk(john)').free(False)
set([Variable('john')])
>>> print lp.parse(r'walk(x)').free(False)
set([Variable('x')])
>>> print lp.parse(r'see(john,mary)').free(False)
set([Variable('john'), Variable('mary')])
>>> print lp.parse(r'exists x.walk(x)').free(False)
set([])
>>> print lp.parse(r'\x.see(john,x)').free(False)
set([Variable('john')])
>>> print lp.parse(r'\x.see(john,x)(mary)').free(False)
set([Variable('john'), Variable('mary')])