Merge pull request #3010 from fernandocar86/iota-operator

Iota operator

AUTHORS.md

@@ -289,6 +289,8 @@
 - Panagiotis Simakis <https://github.com/sp1thas>
 - Richard Wang <https://github.com/richarddwang>
 - Alexandre Perez-Lebel <https://github.com/aperezlebel>
+- Fernando Carranza <https://github.com/fernandocar86>
+- Martin Kondratzky <https://github.com/martinkondra>
 
 ## Others whose work we've taken and included in NLTK, but who didn't directly contribute it:
 

nltk/sem/evaluate.py

@@ -32,6 +32,7 @@
     IffExpression,
     ImpExpression,
     IndividualVariableExpression,
+    IotaExpression,
     LambdaExpression,
     NegatedExpression,
     OrExpression,
@@ -486,6 +487,13 @@ def satisfy(self, parsed, g, trace=None):
                 if self.satisfy(parsed.term, new_g):
                     return True
             return False
+        elif isinstance(parsed, IotaExpression):
+            new_g = g.copy()
+            for u in self.domain:
+                new_g.add(parsed.variable.name, u)
+                if self.satisfy(parsed.term, new_g):
+                    return True
+            return False
         elif isinstance(parsed, LambdaExpression):
             cf = {}
             var = parsed.variable.name

nltk/sem/logic.py

@@ -33,6 +33,8 @@ class Tokens:
     EXISTS_LIST = ["some", "exists", "exist"]
     ALL = "all"
     ALL_LIST = ["all", "forall"]
+    IOTA = "iota"
+    IOTA_LIST = ["iota"]
 
     # Punctuation
     DOT = "."
@@ -58,7 +60,7 @@ class Tokens:
 
     # Collections of tokens
     BINOPS = AND_LIST + OR_LIST + IMP_LIST + IFF_LIST
-    QUANTS = EXISTS_LIST + ALL_LIST
+    QUANTS = EXISTS_LIST + ALL_LIST + IOTA_LIST
     PUNCT = [DOT, OPEN, CLOSE, COMMA]
 
     TOKENS = BINOPS + EQ_LIST + NEQ_LIST + QUANTS + LAMBDA_LIST + PUNCT + NOT_LIST
@@ -90,7 +92,7 @@ def binding_ops():
     Binding operators
     """
     names = ["existential", "universal", "lambda"]
-    for pair in zip(names, [Tokens.EXISTS, Tokens.ALL, Tokens.LAMBDA]):
+    for pair in zip(names, [Tokens.EXISTS, Tokens.ALL, Tokens.LAMBDA, Tokens.IOTA]):
         print("%-15s\t%s" % pair)
 
 
@@ -434,6 +436,8 @@ def get_QuantifiedExpression_factory(self, tok):
             return ExistsExpression
         elif tok in Tokens.ALL_LIST:
             return AllExpression
+        elif tok in Tokens.IOTA_LIST:
+            return IotaExpression
         else:
             self.assertToken(tok, Tokens.QUANTS)
 
@@ -1755,6 +1759,11 @@ def getQuantifier(self):
         return Tokens.ALL
 
 
+class IotaExpression(QuantifiedExpression):
+    def getQuantifier(self):
+        return Tokens.IOTA
+
+
 class NegatedExpression(Expression):
     def __init__(self, term):
         assert isinstance(term, Expression), "%s is not an Expression" % term