.. Copyright (C) 2001-2010 NLTK Project
.. For license information, see LICENSE.TXT

=======================
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.

--------
Overview
--------

    >>> from nltk.sem.logic import *

The default inventory of logical constants is the following:

    >>> boolean_ops() # doctest: +NORMALIZE_WHITESPACE
    negation           -
    conjunction        &
    disjunction        |
    implication        ->
    equivalence        <->
    >>> equality_preds() # doctest: +NORMALIZE_WHITESPACE
    equality           =
    inequality         !=
    >>> binding_ops() # doctest: +NORMALIZE_WHITESPACE
    existential        exists
    universal          all
    lambda             \
    
----------------
Regression Tests
----------------


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'(man(x) & (tall(x) & walks(x)))')
    (man(x) & (tall(x) & walks(x)))
    >>> print lp.parse(r'P(x) -> Q(x) <-> R(x) | S(x) & T(x)')
    ((P(x) -> Q(x)) <-> (R(x) | (S(x) & T(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))
    >>> print lp.parse(r'exists x.(man(x) & tall(x) & walks(x))')
    exists x.((man(x) & tall(x)) & walks(x))
    >>> print lp.parse(r'-P(x) & Q(x)')
    (-P(x) & Q(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
    >>> print lp.parse(r'exists x.x = y')
    exists x.(x = y)
    >>> print lp.parse(r'A != B')
    -(A = B)
    >>> print lp.parse('P(x) & x=y & P(y)')
    ((P(x) & (x = y)) & P(y))
    >>> try: print lp.parse(r'\walk.walk(x)')
    ... except ParseException,e: print e
    'walk' is an illegal variable name.  Constants may not be abstracted.
    \walk.walk(x)
     ^
    >>> try: print lp.parse(r'all walk.walk(john)')
    ... except ParseException,e: print e
    'walk' is an illegal variable name.  Constants may not be quantified.
    all walk.walk(john)
        ^
    >>> 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.
    x(john)
    ^
    
    >>> 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 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))

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() # doctest: +ELLIPSIS
    {...}
    >>> c.first.type
    t
    
    >>> a = tlp.parse('P(x)')
    >>> b = tlp.parse('P(x) & Q(x)')
    >>> a.type
    ?
    >>> typecheck([a,b]) # doctest: +ELLIPSIS
    {...}
    >>> 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() # doctest: +ELLIPSIS
    {...}
    >>> b.typecheck() # doctest: +ELLIPSIS
    {...}
    >>> 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) # doctest: +ELLIPSIS
    {...}
    >>> try: typecheck([a,b], signature)
    ... except InconsistentTypeHierarchyException, e: print e
    The variable 'P' was found in multiple places with different types.

Parse errors
============

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

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