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

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

`betaConversionTestSuite.pl`

Tests based on Blackburn & Bos' book, 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))))(\f.walk(f))(\f.talk(f))').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.\f.love(d,f))))(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)
>>> try: print lp.parse(r'\walk.walk(x)')
... except ParseException,e: print e
'walk' is an illegal variable name.  Constants may not be abstracted.
>>> try: print lp.parse(r'all walk.walk(john)')
... except ParseException,e: print e
'walk' is an illegal variable name.  Constant expressions may not be quantified.
>>> try: print lp.parse(r'x(john)')
... except ParseException,e: print e
'x' is an illegal predicate name.  Individual variables may not be used as predicates.

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)

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

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')])

normalize

>>> print lp.parse(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 *
>>> tlp = LogicParser(True)

.type

>>> 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 e.typecheck()
{'x': e, 'man': <e,?>}
>>> sig = {'man': '<e, t>'}
>>> e = tlp.parse(r'man(x)', sig)
>>> print e.function.type
<e,t>
>>> print e.typecheck()
{'x': e, 'man': <e,t>}
>>> print e.function.type
<e,t>
>>> print e.typecheck(sig)
{'x': e, 'man': <e,t>}

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, 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, 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, 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, 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, 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, e: print e
The variable 'P' was found in multiple places with different types.