Logic & Lambda Calculus

The nltk.logic package allows expressions of First-Order Logic (FOL) to be parsed into Expression objects. In addition to FOL, the parser handles lambda-abstraction with variables of higher order.

1 Overview

>>> from nltk.sem.logic import *

The default inventory of logical constants is the following:

>>> boolean_ops() 
negation           -
conjunction        &
disjunction        |
implication        ->
equivalence        <->
>>> equality_preds() 
equality           =
inequality         !=
>>> binding_ops() 
existential        exists
universal          all
lambda             \

2 Regression Tests

2.1 Untyped Logic

Process logical expressions conveniently:

>>> lexpr = Expression.fromstring

Test for equality under alpha-conversion

>>> e1 = lexpr('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 = lexpr(r'\X.\X.X(X)(1)').simplify()
>>> id = lexpr(r'\X.X(X)')
>>> l == id
True

Test numerals

>>> 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()
>>> 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 = lexpr(r'john')
>>> man = lexpr(r'\x.man(x)')
>>> walk = lexpr(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)>

`betaConversionTestSuite.pl`

Tests based on Blackburn & Bos' book, Representation and Inference for Natural Language.

>>> x1 = lexpr(r'\P.P(mia)(\x.walk(x))').simplify()
>>> x2 = lexpr(r'walk(mia)').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'exists x.(man(x) & ((\P.exists x.(woman(x) & P(x)))(\y.love(x,y))))').simplify()
>>> x2 = lexpr(r'exists x.(man(x) & exists y.(woman(y) & love(x,y)))').simplify()
>>> x1 == x2
True
>>> x1 = lexpr(r'\a.sleep(a)(mia)').simplify()
>>> x2 = lexpr(r'sleep(mia)').simplify()
>>> x1 == x2
True
>>> x1 = lexpr(r'\a.\b.like(b,a)(mia)').simplify()
>>> x2 = lexpr(r'\b.like(b,mia)').simplify()
>>> x1 == x2
True
>>> x1 = lexpr(r'\a.(\b.like(b,a)(vincent))').simplify()
>>> x2 = lexpr(r'\a.like(vincent,a)').simplify()
>>> x1 == x2
True
>>> x1 = lexpr(r'\a.((\b.like(b,a)(vincent)) & sleep(a))').simplify()
>>> x2 = lexpr(r'\a.(like(vincent,a) & sleep(a))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'(\a.\b.like(b,a)(mia)(vincent))').simplify()
>>> x2 = lexpr(r'like(vincent,mia)').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'P((\a.sleep(a)(vincent)))').simplify()
>>> x2 = lexpr(r'P(sleep(vincent))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'\A.A((\b.sleep(b)(vincent)))').simplify()
>>> x2 = lexpr(r'\A.A(sleep(vincent))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'\A.A(sleep(vincent))').simplify()
>>> x2 = lexpr(r'\A.A(sleep(vincent))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'(\A.A(vincent)(\b.sleep(b)))').simplify()
>>> x2 = lexpr(r'sleep(vincent)').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'\A.believe(mia,A(vincent))(\b.sleep(b))').simplify()
>>> x2 = lexpr(r'believe(mia,sleep(vincent))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'(\A.(A(vincent) & A(mia)))(\b.sleep(b))').simplify()
>>> x2 = lexpr(r'(sleep(vincent) & sleep(mia))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'\A.\B.(\C.C(A(vincent))(\d.probably(d)) & (\C.C(B(mia))(\d.improbably(d))))(\f.walk(f))(\f.talk(f))').simplify()
>>> x2 = lexpr(r'(probably(walk(vincent)) & improbably(talk(mia)))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'(\a.\b.(\C.C(a,b)(\d.\f.love(d,f))))(jules)(mia)').simplify()
>>> x2 = lexpr(r'love(jules,mia)').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'(\A.\B.exists c.(A(c) & B(c)))(\d.boxer(d),\d.sleep(d))').simplify()
>>> x2 = lexpr(r'exists c.(boxer(c) & sleep(c))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'\A.Z(A)(\c.\a.like(a,c))').simplify()
>>> x2 = lexpr(r'Z(\c.\a.like(a,c))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'\A.\b.A(b)(\c.\b.like(b,c))').simplify()
>>> x2 = lexpr(r'\b.(\c.\b.like(b,c)(b))').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'(\a.\b.(\C.C(a,b)(\b.\a.loves(b,a))))(jules)(mia)').simplify()
>>> x2 = lexpr(r'loves(jules,mia)').simplify()
>>> x1 == x2
True

>>> x1 = lexpr(r'(\A.\b.(exists b.A(b) & A(b)))(\c.boxer(c))(vincent)').simplify()
>>> x2 = lexpr(r'((exists b.boxer(b)) & boxer(vincent))').simplify()
>>> x1 == x2
True

Test Parser

>>> print(lexpr(r'john'))
john
>>> print(lexpr(r'x'))
x
>>> print(lexpr(r'-man(x)'))
-man(x)
>>> print(lexpr(r'--man(x)'))
--man(x)
>>> print(lexpr(r'(man(x))'))
man(x)
>>> print(lexpr(r'((man(x)))'))
man(x)
>>> print(lexpr(r'man(x) <-> tall(x)'))
(man(x) <-> tall(x))
>>> print(lexpr(r'(man(x) <-> tall(x))'))
(man(x) <-> tall(x))
>>> print(lexpr(r'(man(x) & tall(x) & walks(x))'))
(man(x) & tall(x) & walks(x))
>>> print(lexpr(r'(man(x) & tall(x) & walks(x))').first)
(man(x) & tall(x))
>>> print(lexpr(r'man(x) | tall(x) & walks(x)'))
(man(x) | (tall(x) & walks(x)))
>>> print(lexpr(r'((man(x) & tall(x)) | walks(x))'))
((man(x) & tall(x)) | walks(x))
>>> print(lexpr(r'man(x) & (tall(x) | walks(x))'))
(man(x) & (tall(x) | walks(x)))
>>> print(lexpr(r'(man(x) & (tall(x) | walks(x)))'))
(man(x) & (tall(x) | walks(x)))
>>> print(lexpr(r'P(x) -> Q(x) <-> R(x) | S(x) & T(x)'))
((P(x) -> Q(x)) <-> (R(x) | (S(x) & T(x))))
>>> print(lexpr(r'exists x.man(x)'))
exists x.man(x)
>>> print(lexpr(r'exists x.(man(x) & tall(x))'))
exists x.(man(x) & tall(x))
>>> print(lexpr(r'exists x.(man(x) & tall(x) & walks(x))'))
exists x.(man(x) & tall(x) & walks(x))
>>> print(lexpr(r'-P(x) & Q(x)'))
(-P(x) & Q(x))
>>> lexpr(r'-P(x) & Q(x)') == lexpr(r'(-P(x)) & Q(x)')
True
>>> print(lexpr(r'\x.man(x)'))
\x.man(x)
>>> print(lexpr(r'\x.man(x)(john)'))
\x.man(x)(john)
>>> print(lexpr(r'\x.man(x)(john) & tall(x)'))
(\x.man(x)(john) & tall(x))
>>> print(lexpr(r'\x.\y.sees(x,y)'))
\x y.sees(x,y)
>>> print(lexpr(r'\x  y.sees(x,y)'))
\x y.sees(x,y)
>>> print(lexpr(r'\x.\y.sees(x,y)(a)'))
(\x y.sees(x,y))(a)
>>> print(lexpr(r'\x  y.sees(x,y)(a)'))
(\x y.sees(x,y))(a)
>>> print(lexpr(r'\x.\y.sees(x,y)(a)(b)'))
((\x y.sees(x,y))(a))(b)
>>> print(lexpr(r'\x  y.sees(x,y)(a)(b)'))
((\x y.sees(x,y))(a))(b)
>>> print(lexpr(r'\x.\y.sees(x,y)(a,b)'))
((\x y.sees(x,y))(a))(b)
>>> print(lexpr(r'\x  y.sees(x,y)(a,b)'))
((\x y.sees(x,y))(a))(b)
>>> print(lexpr(r'((\x.\y.sees(x,y))(a))(b)'))
((\x y.sees(x,y))(a))(b)
>>> print(lexpr(r'P(x)(y)(z)'))
P(x,y,z)
>>> print(lexpr(r'P(Q)'))
P(Q)
>>> print(lexpr(r'P(Q(x))'))
P(Q(x))
>>> print(lexpr(r'(\x.exists y.walks(x,y))(x)'))
(\x.exists y.walks(x,y))(x)
>>> print(lexpr(r'exists x.(x = john)'))
exists x.(x = john)
>>> print(lexpr(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 = lexpr(r'exists c.exists b.A(b,c) & A(b,c)')
>>> b = lexpr(r'(exists c.(exists b.A(b,c))) & A(b,c)')
>>> print(a == b)
True
>>> a = lexpr(r'exists c.(exists b.A(b,c) & A(b,c))')
>>> b = lexpr(r'exists c.((exists b.A(b,c)) & A(b,c))')
>>> print(a == b)
True
>>> print(lexpr(r'exists x.x = y'))
exists x.(x = y)
>>> print(lexpr('A(B)(C)'))
A(B,C)
>>> print(lexpr('(A(B))(C)'))
A(B,C)
>>> print(lexpr('A((B)(C))'))
A(B(C))
>>> print(lexpr('A(B(C))'))
A(B(C))
>>> print(lexpr('(A)(B(C))'))
A(B(C))
>>> print(lexpr('(((A)))(((B))(((C))))'))
A(B(C))
>>> print(lexpr(r'A != B'))
-(A = B)
>>> print(lexpr('P(x) & x=y & P(y)'))
(P(x) & (x = y) & P(y))
>>> try: print(lexpr(r'\walk.walk(x)'))
... except LogicalExpressionException as e: print(e)
'walk' is an illegal variable name.  Constants may not be abstracted.
\walk.walk(x)
 ^
>>> try: print(lexpr(r'all walk.walk(john)'))
... except LogicalExpressionException as e: print(e)
'walk' is an illegal variable name.  Constants may not be quantified.
all walk.walk(john)
    ^
>>> try: print(lexpr(r'x(john)'))
... except LogicalExpressionException as e: print(e)
'x' is an illegal predicate name.  Individual variables may not be used as predicates.
x(john)
^

>>> from nltk.sem.logic import _LogicParser # hack to give access to custom quote chars
>>> lpq = _LogicParser()
>>> lpq.quote_chars = [("'", "'", "\\", False)]
>>> print(lpq.parse(r"(man(x) & 'tall\'s,' (x) & walks (x) )"))
(man(x) & tall's,(x) & walks(x))
>>> lpq.quote_chars = [("'", "'", "\\", True)]
>>> print(lpq.parse(r"'tall\'s,'"))
'tall\'s,'
>>> print(lpq.parse(r"'spaced name(x)'"))
'spaced name(x)'
>>> print(lpq.parse(r"-'tall\'s,'(x)"))
-'tall\'s,'(x)
>>> print(lpq.parse(r"(man(x) & 'tall\'s,' (x) & walks (x) )"))
(man(x) & 'tall\'s,'(x) & walks(x))

Simplify

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

Replace

>>> a = lexpr(r'a')
>>> x = lexpr(r'x')
>>> y = lexpr(r'y')
>>> z = lexpr(r'z')

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

>>> from nltk.sem import logic
>>> logic._counter._value = 0
>>> e1 = lexpr('e1')
>>> e2 = lexpr('e2')
>>> print(lexpr('exists e1 e2.(walk(e1) & talk(e2))').replace(e1.variable, e2, True))
exists e2 e01.(walk(e2) & talk(e01))

Variables / Free

>>> examples = [r'walk(john)',
...             r'walk(x)',
...             r'?vp(?np)',
...             r'see(john,mary)',
...             r'exists x.walk(x)',
...             r'\x.see(john,x)',
...             r'\x.see(john,x)(mary)',
...             r'P(x)',
...             r'\P.P(x)',
...             r'aa(x,bb(y),cc(z),P(w),u)',
...             r'bo(?det(?n),@x)']
>>> examples = [lexpr(e) for e in examples]

>>> for e in examples:
...     print('%-25s' % e, sorted(e.free()))
walk(john)                []
walk(x)                   [Variable('x')]
?vp(?np)                  []
see(john,mary)            []
exists x.walk(x)          []
\x.see(john,x)            []
(\x.see(john,x))(mary)    []
P(x)                      [Variable('P'), Variable('x')]
\P.P(x)                   [Variable('x')]
aa(x,bb(y),cc(z),P(w),u)  [Variable('P'), Variable('u'), Variable('w'), Variable('x'), Variable('y'), Variable('z')]
bo(?det(?n),@x)           []

>>> for e in examples:
...     print('%-25s' % e, sorted(e.constants()))
walk(john)                [Variable('john')]
walk(x)                   []
?vp(?np)                  [Variable('?np')]
see(john,mary)            [Variable('john'), Variable('mary')]
exists x.walk(x)          []
\x.see(john,x)            [Variable('john')]
(\x.see(john,x))(mary)    [Variable('john'), Variable('mary')]
P(x)                      []
\P.P(x)                   []
aa(x,bb(y),cc(z),P(w),u)  []
bo(?det(?n),@x)           [Variable('?n'), Variable('@x')]

>>> for e in examples:
...     print('%-25s' % e, sorted(e.predicates()))
walk(john)                [Variable('walk')]
walk(x)                   [Variable('walk')]
?vp(?np)                  [Variable('?vp')]
see(john,mary)            [Variable('see')]
exists x.walk(x)          [Variable('walk')]
\x.see(john,x)            [Variable('see')]
(\x.see(john,x))(mary)    [Variable('see')]
P(x)                      []
\P.P(x)                   []
aa(x,bb(y),cc(z),P(w),u)  [Variable('aa'), Variable('bb'), Variable('cc')]
bo(?det(?n),@x)           [Variable('?det'), Variable('bo')]

>>> for e in examples:
...     print('%-25s' % e, sorted(e.variables()))
walk(john)                []
walk(x)                   [Variable('x')]
?vp(?np)                  [Variable('?np'), Variable('?vp')]
see(john,mary)            []
exists x.walk(x)          []
\x.see(john,x)            []
(\x.see(john,x))(mary)    []
P(x)                      [Variable('P'), Variable('x')]
\P.P(x)                   [Variable('x')]
aa(x,bb(y),cc(z),P(w),u)  [Variable('P'), Variable('u'), Variable('w'), Variable('x'), Variable('y'), Variable('z')]
bo(?det(?n),@x)           [Variable('?det'), Variable('?n'), Variable('@x')]

normalize

>>> print(lexpr(r'\e083.(walk(e083, z472) & talk(e092, z938))').normalize())
\e01.(walk(e01,z3) & talk(e02,z4))

2.2 Typed Logic

>>> from nltk.sem.logic import _LogicParser
>>> tlp = _LogicParser(True)
>>> print(tlp.parse(r'man(x)').type)
?
>>> print(tlp.parse(r'walk(angus)').type)
?
>>> print(tlp.parse(r'-man(x)').type)
t
>>> print(tlp.parse(r'(man(x) <-> tall(x))').type)
t
>>> print(tlp.parse(r'exists x.(man(x) & tall(x))').type)
t
>>> print(tlp.parse(r'\x.man(x)').type)
<e,?>
>>> print(tlp.parse(r'john').type)
e
>>> print(tlp.parse(r'\x y.sees(x,y)').type)
<e,<e,?>>
>>> print(tlp.parse(r'\x.man(x)(john)').type)
?
>>> print(tlp.parse(r'\x.\y.sees(x,y)(john)').type)
<e,?>
>>> print(tlp.parse(r'\x.\y.sees(x,y)(john)(mary)').type)
?
>>> print(tlp.parse(r'\P.\Q.exists x.(P(x) & Q(x))').type)
<<e,t>,<<e,t>,t>>
>>> print(tlp.parse(r'\x.y').type)
<?,e>
>>> print(tlp.parse(r'\P.P(x)').type)
<<e,?>,?>

>>> parsed = tlp.parse('see(john,mary)')
>>> print(parsed.type)
?
>>> print(parsed.function)
see(john)
>>> print(parsed.function.type)
<e,?>
>>> print(parsed.function.function)
see
>>> print(parsed.function.function.type)
<e,<e,?>>

>>> parsed = tlp.parse('P(x,y)')
>>> print(parsed)
P(x,y)
>>> print(parsed.type)
?
>>> print(parsed.function)
P(x)
>>> print(parsed.function.type)
<e,?>
>>> print(parsed.function.function)
P
>>> print(parsed.function.function.type)
<e,<e,?>>

>>> print(tlp.parse(r'P').type)
?

>>> print(tlp.parse(r'P', {'P': 't'}).type)
t

>>> a = tlp.parse(r'P(x)')
>>> print(a.type)
?
>>> print(a.function.type)
<e,?>
>>> print(a.argument.type)
e

>>> a = tlp.parse(r'-P(x)')
>>> print(a.type)
t
>>> print(a.term.type)
t
>>> print(a.term.function.type)
<e,t>
>>> print(a.term.argument.type)
e

>>> a = tlp.parse(r'P & Q')
>>> print(a.type)
t
>>> print(a.first.type)
t
>>> print(a.second.type)
t

>>> a = tlp.parse(r'(P(x) & Q(x))')
>>> print(a.type)
t
>>> print(a.first.type)
t
>>> print(a.first.function.type)
<e,t>
>>> print(a.first.argument.type)
e
>>> print(a.second.type)
t
>>> print(a.second.function.type)
<e,t>
>>> print(a.second.argument.type)
e

>>> a = tlp.parse(r'\x.P(x)')
>>> print(a.type)
<e,?>
>>> print(a.term.function.type)
<e,?>
>>> print(a.term.argument.type)
e

>>> a = tlp.parse(r'\P.P(x)')
>>> print(a.type)
<<e,?>,?>
>>> print(a.term.function.type)
<e,?>
>>> print(a.term.argument.type)
e

>>> a = tlp.parse(r'(\x.P(x)(john)) & Q(x)')
>>> print(a.type)
t
>>> print(a.first.type)
t
>>> print(a.first.function.type)
<e,t>
>>> print(a.first.function.term.function.type)
<e,t>
>>> print(a.first.function.term.argument.type)
e
>>> print(a.first.argument.type)
e

>>> a = tlp.parse(r'\x y.P(x,y)(john)(mary) & Q(x)')
>>> print(a.type)
t
>>> print(a.first.type)
t
>>> print(a.first.function.type)
<e,t>
>>> print(a.first.function.function.type)
<e,<e,t>>

>>> a = tlp.parse(r'--P')
>>> print(a.type)
t
>>> print(a.term.type)
t
>>> print(a.term.term.type)
t

>>> tlp.parse(r'\x y.P(x,y)').type
<e,<e,?>>
>>> tlp.parse(r'\x y.P(x,y)', {'P': '<e,<e,t>>'}).type
<e,<e,t>>

>>> a = tlp.parse(r'\P y.P(john,y)(\x y.see(x,y))')
>>> a.type
<e,?>
>>> a.function.type
<<e,<e,?>>,<e,?>>
>>> a.function.term.term.function.function.type
<e,<e,?>>
>>> a.argument.type
<e,<e,?>>

>>> a = tlp.parse(r'exists c f.(father(c) = f)')
>>> a.type
t
>>> a.term.term.type
t
>>> a.term.term.first.type
e
>>> a.term.term.first.function.type
<e,e>
>>> a.term.term.second.type
e

typecheck()

>>> a = tlp.parse('P(x)')
>>> b = tlp.parse('Q(x)')
>>> a.type
?
>>> c = a & b
>>> c.first.type
?
>>> c.typecheck() 
{...}
>>> c.first.type
t

>>> a = tlp.parse('P(x)')
>>> b = tlp.parse('P(x) & Q(x)')
>>> a.type
?
>>> typecheck([a,b]) 
{...}
>>> a.type
t

>>> e = tlp.parse(r'man(x)')
>>> print(dict((k,str(v)) for k,v in e.typecheck().items()) == {'x': 'e', 'man': '<e,?>'})
True
>>> sig = {'man': '<e, t>'}
>>> e = tlp.parse(r'man(x)', sig)
>>> print(e.function.type)
<e,t>
>>> print(dict((k,str(v)) for k,v in e.typecheck().items()) == {'x': 'e', 'man': '<e,t>'})
True
>>> print(e.function.type)
<e,t>
>>> print(dict((k,str(v)) for k,v in e.typecheck(sig).items()) == {'x': 'e', 'man': '<e,t>'})
True

findtype()

>>> print(tlp.parse(r'man(x)').findtype(Variable('man')))
<e,?>
>>> print(tlp.parse(r'see(x,y)').findtype(Variable('see')))
<e,<e,?>>
>>> print(tlp.parse(r'P(Q(R(x)))').findtype(Variable('Q')))
?

parse_type()

>>> print(parse_type('e'))
e
>>> print(parse_type('<e,t>'))
<e,t>
>>> print(parse_type('<<e,t>,<e,t>>'))
<<e,t>,<e,t>>
>>> print(parse_type('<<e,?>,?>'))
<<e,?>,?>

alternative type format

>>> print(parse_type('e').str())
IND
>>> print(parse_type('<e,?>').str())
(IND -> ANY)
>>> print(parse_type('<<e,t>,t>').str())
((IND -> BOOL) -> BOOL)

Type.__eq__()

>>> from nltk.sem.logic import *

>>> e = ENTITY_TYPE
>>> t = TRUTH_TYPE
>>> a = ANY_TYPE
>>> et = ComplexType(e,t)
>>> eet = ComplexType(e,ComplexType(e,t))
>>> at = ComplexType(a,t)
>>> ea = ComplexType(e,a)
>>> aa = ComplexType(a,a)

>>> e == e
True
>>> t == t
True
>>> e == t
False
>>> a == t
False
>>> t == a
False
>>> a == a
True
>>> et == et
True
>>> a == et
False
>>> et == a
False
>>> a == ComplexType(a,aa)
True
>>> ComplexType(a,aa) == a
True

matches()

>>> e.matches(t)
False
>>> a.matches(t)
True
>>> t.matches(a)
True
>>> a.matches(et)
True
>>> et.matches(a)
True
>>> ea.matches(eet)
True
>>> eet.matches(ea)
True
>>> aa.matches(et)
True
>>> aa.matches(t)
True

Type error during parsing

>>> try: print(tlp.parse(r'exists x y.(P(x) & P(x,y))'))
... except InconsistentTypeHierarchyException as e: print(e)
The variable 'P' was found in multiple places with different types.
>>> try: tlp.parse(r'\x y.see(x,y)(\x.man(x))')
... except TypeException as e: print(e)
The function '\x y.see(x,y)' is of type '<e,<e,?>>' and cannot be applied to '\x.man(x)' of type '<e,?>'.  Its argument must match type 'e'.
>>> try: tlp.parse(r'\P x y.-P(x,y)(\x.-man(x))')
... except TypeException as e: print(e)
The function '\P x y.-P(x,y)' is of type '<<e,<e,t>>,<e,<e,t>>>' and cannot be applied to '\x.-man(x)' of type '<e,t>'.  Its argument must match type '<e,<e,t>>'.

>>> a = tlp.parse(r'-talk(x)')
>>> signature = a.typecheck()
>>> try: print(tlp.parse(r'-talk(x,y)', signature))
... except InconsistentTypeHierarchyException as e: print(e)
The variable 'talk' was found in multiple places with different types.

>>> a = tlp.parse(r'-P(x)')
>>> b = tlp.parse(r'-P(x,y)')
>>> a.typecheck() 
{...}
>>> b.typecheck() 
{...}
>>> try: typecheck([a,b])
... except InconsistentTypeHierarchyException as e: print(e)
The variable 'P' was found in multiple places with different types.

>>> a = tlp.parse(r'P(x)')
>>> b = tlp.parse(r'P(x,y)')
>>> signature = {'P': '<e,t>'}
>>> a.typecheck(signature) 
{...}
>>> try: typecheck([a,b], signature)
... except InconsistentTypeHierarchyException as e: print(e)
The variable 'P' was found in multiple places with different types.

Parse errors

>>> try: lexpr(r'')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.

^
>>> try: lexpr(r'(')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
(
 ^
>>> try: lexpr(r')')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
)
^
>>> try: lexpr(r'()')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
()
 ^
>>> try: lexpr(r'(P(x) & Q(x)')
... except LogicalExpressionException as e: print(e)
End of input found.  Expected token ')'.
(P(x) & Q(x)
            ^
>>> try: lexpr(r'(P(x) &')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
(P(x) &
       ^
>>> try: lexpr(r'(P(x) | )')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
(P(x) | )
        ^
>>> try: lexpr(r'P(x) ->')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
P(x) ->
       ^
>>> try: lexpr(r'P(x')
... except LogicalExpressionException as e: print(e)
End of input found.  Expected token ')'.
P(x
   ^
>>> try: lexpr(r'P(x,')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
P(x,
    ^
>>> try: lexpr(r'P(x,)')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
P(x,)
    ^
>>> try: lexpr(r'exists')
... except LogicalExpressionException as e: print(e)
End of input found.  Variable and Expression expected following quantifier 'exists'.
exists
       ^
>>> try: lexpr(r'exists x')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
exists x
         ^
>>> try: lexpr(r'exists x.')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
exists x.
         ^
>>> try: lexpr(r'\  ')
... except LogicalExpressionException as e: print(e)
End of input found.  Variable and Expression expected following lambda operator.
\
  ^
>>> try: lexpr(r'\ x')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
\ x
    ^
>>> try: lexpr(r'\ x y')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
\ x y
      ^
>>> try: lexpr(r'\ x.')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
\ x.
    ^
>>> try: lexpr(r'P(x)Q(x)')
... except LogicalExpressionException as e: print(e)
Unexpected token: 'Q'.
P(x)Q(x)
    ^
>>> try: lexpr(r'(P(x)Q(x)')
... except LogicalExpressionException as e: print(e)
Unexpected token: 'Q'.  Expected token ')'.
(P(x)Q(x)
     ^
>>> try: lexpr(r'exists x y')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
exists x y
           ^
>>> try: lexpr(r'exists x y.')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
exists x y.
           ^
>>> try: lexpr(r'exists x -> y')
... except LogicalExpressionException as e: print(e)
Unexpected token: '->'.  Expression expected.
exists x -> y
         ^

>>> try: lexpr(r'A -> ((P(x) & Q(x)) -> Z')
... except LogicalExpressionException as e: print(e)
End of input found.  Expected token ')'.
A -> ((P(x) & Q(x)) -> Z
                        ^
>>> try: lexpr(r'A -> ((P(x) &) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> ((P(x) &) -> Z
             ^
>>> try: lexpr(r'A -> ((P(x) | )) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> ((P(x) | )) -> Z
              ^
>>> try: lexpr(r'A -> (P(x) ->) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (P(x) ->) -> Z
             ^
>>> try: lexpr(r'A -> (P(x) -> Z')
... except LogicalExpressionException as e: print(e)
End of input found.  Expected token ')'.
A -> (P(x) -> Z
               ^
>>> try: lexpr(r'A -> (P(x,) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (P(x,) -> Z
          ^
>>> try: lexpr(r'A -> (P(x,)) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (P(x,)) -> Z
          ^
>>> try: lexpr(r'A -> (exists) -> Z')
... except LogicalExpressionException as e: print(e)
')' is an illegal variable name.  Constants may not be quantified.
A -> (exists) -> Z
            ^
>>> try: lexpr(r'A -> (exists x) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (exists x) -> Z
              ^
>>> try: lexpr(r'A -> (exists x.) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (exists x.) -> Z
               ^
>>> try: lexpr(r'A -> (\  ) -> Z')
... except LogicalExpressionException as e: print(e)
')' is an illegal variable name.  Constants may not be abstracted.
A -> (\  ) -> Z
         ^
>>> try: lexpr(r'A -> (\ x) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (\ x) -> Z
         ^
>>> try: lexpr(r'A -> (\ x y) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (\ x y) -> Z
           ^
>>> try: lexpr(r'A -> (\ x.) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (\ x.) -> Z
          ^
>>> try: lexpr(r'A -> (P(x)Q(x)) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: 'Q'.  Expected token ')'.
A -> (P(x)Q(x)) -> Z
          ^
>>> try: lexpr(r'A -> ((P(x)Q(x)) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: 'Q'.  Expected token ')'.
A -> ((P(x)Q(x)) -> Z
           ^
>>> try: lexpr(r'A -> (all x y) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (all x y) -> Z
             ^
>>> try: lexpr(r'A -> (exists x y.) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (exists x y.) -> Z
                 ^
>>> try: lexpr(r'A -> (exists x -> y) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: '->'.  Expression expected.
A -> (exists x -> y) -> Z
               ^