natural language toolkit linear logic dan garrette dhgarrettegmail com c 20012023 nltk project url https www nltk org for license information see license txt punctuation operations a linear logic expression parser def initself logicparser initself self operatorprecedence app 1 tokens imp 2 none 3 self rightassociatedoperations tokens imp def getallsymbolsself return tokens tokens def handleself tok context if tok not in tokens tokens return self handlevariabletok context elif tok tokens open return self handleopentok context def getbooleanexpressionfactoryself tok if tok tokens imp return impexpression else return none def makebooleanexpressionself factory first second return factoryfirst second def attemptapplicationexpressionself expression context param name str for the constant name param dependencies list of int for the indices on which this atom is dependent if self is bound by bindings return the atomic to which it is bound otherwise return self param bindings bindingdict a dictionary of bindings used to simplify return atomicexpression from iddo lev s phd dissertation p108109 param indexcounter counter for unique indices param glueformulafactory glueformula for creating new glue formulas return expression set for the compiled linear logic and any newly created glue formulas from iddo lev s phd dissertation p108109 param indexcounter counter for unique indices param glueformulafactory glueformula for creating new glue formulas return expression set for the compiled linear logic and any newly created glue formulas if other is a constant then it must be equal to self if other is a variable then it must not be bound to anything other than self param other expression param bindings bindingdict a dictionary of all current bindings return bindingdict a new combined dictionary of of bindings and any new binding raise unificationexception if self and other cannot be unified in the context of bindings self must not be bound to anything other than other param other expression param bindings bindingdict a dictionary of all current bindings return bindingdict a new combined dictionary of of bindings and the new binding raise unificationexception if self and other cannot be unified in the context of bindings param antecedent expression for the antecedent param consequent expression for the consequent both the antecedent and consequent of self and other must unify param other impexpression param bindings bindingdict a dictionary of all current bindings return bindingdict a new combined dictionary of of bindings and any new bindings raise unificationexception if self and other cannot be unified in the context of bindings from iddo lev s phd dissertation p108109 param indexcounter counter for unique indices param glueformulafactory glueformula for creating new glue formulas return expression set for the compiled linear logic and any newly created glue formulas from iddo lev s phd dissertation p108109 param indexcounter counter for unique indices param glueformulafactory glueformula for creating new glue formulas return expression list of glueformula for the compiled linear logic and any newly created glue formulas param function expression for the function param argument expression for the argument param argumentindices set for the indices of the glue formula from which the argument came raise linearlogicapplicationexception if function cannot be applied to argument given argumentindices if you are running it on complied premises more conditions apply a dependencies of a o b o c must be a proper subset of argumentindices since function is an implication return its consequent there should be no need to check that the application is valid since the checking is done by the constructor param bindings bindingdict a dictionary of bindings used to simplify return expression param bindings list variableexpression atomicexpression to initialize the dictionary dict variableexpression atomicexpression to initialize the dictionary a binding is consistent with the dict if its variable is not already bound or if its variable is already bound to its argument param variable variableexpression the variable bind param binding expression the expression to which variable should be bound raise variablebindingexception if the variable cannot be bound in this dictionary return the expression to which variable is bound param other bindingdict the dict with which to combine self return bindingdict a new dict containing all the elements of both parameters raise variablebindingexception if the parameter dictionaries are not consistent with each other natural language toolkit linear logic dan garrette dhgarrette gmail com c 2001 2023 nltk project url https www nltk org for license information see license txt punctuation operations a linear logic expression parser attempt to make an application expression if the next tokens are an argument in parens then the argument expression is a function being applied to the arguments otherwise return the argument expression swallow then open paren param name str for the constant name param dependencies list of int for the indices on which this atom is dependent if self is bound by bindings return the atomic to which it is bound otherwise return self param bindings bindingdict a dictionary of bindings used to simplify return atomicexpression from iddo lev s phd dissertation p108 109 param index_counter counter for unique indices param glueformulafactory glueformula for creating new glue formulas return expression set for the compiled linear logic and any newly created glue formulas from iddo lev s phd dissertation p108 109 param index_counter counter for unique indices param glueformulafactory glueformula for creating new glue formulas return expression set for the compiled linear logic and any newly created glue formulas if other is a constant then it must be equal to self if other is a variable then it must not be bound to anything other than self param other expression param bindings bindingdict a dictionary of all current bindings return bindingdict a new combined dictionary of of bindings and any new binding raise unificationexception if self and other cannot be unified in the context of bindings self must not be bound to anything other than other param other expression param bindings bindingdict a dictionary of all current bindings return bindingdict a new combined dictionary of of bindings and the new binding raise unificationexception if self and other cannot be unified in the context of bindings param antecedent expression for the antecedent param consequent expression for the consequent both the antecedent and consequent of self and other must unify param other impexpression param bindings bindingdict a dictionary of all current bindings return bindingdict a new combined dictionary of of bindings and any new bindings raise unificationexception if self and other cannot be unified in the context of bindings from iddo lev s phd dissertation p108 109 param index_counter counter for unique indices param glueformulafactory glueformula for creating new glue formulas return expression set for the compiled linear logic and any newly created glue formulas from iddo lev s phd dissertation p108 109 param index_counter counter for unique indices param glueformulafactory glueformula for creating new glue formulas return expression list of glueformula for the compiled linear logic and any newly created glue formulas param function expression for the function param argument expression for the argument param argument_indices set for the indices of the glue formula from which the argument came raise linearlogicapplicationexception if function cannot be applied to argument given argument_indices if you are running it on complied premises more conditions apply a dependencies of a o b o c must be a proper subset of argument_indices since function is an implication return its consequent there should be no need to check that the application is valid since the checking is done by the constructor param bindings bindingdict a dictionary of bindings used to simplify return expression param bindings list variableexpression atomicexpression to initialize the dictionary dict variableexpression atomicexpression to initialize the dictionary a binding is consistent with the dict if its variable is not already bound or if its variable is already bound to its argument param variable variableexpression the variable bind param binding expression the expression to which variable should be bound raise variablebindingexception if the variable cannot be bound in this dictionary return the expression to which variable is bound param other bindingdict the dict with which to combine self return bindingdict a new dict containing all the elements of both parameters raise variablebindingexception if the parameter dictionaries are not consistent with each other
from nltk.internals import Counter
from nltk.sem.logic import APP, LogicParser

_counter = Counter()


class Tokens:
    
    OPEN = "("
    CLOSE = ")"

    
    IMP = "-o"

    PUNCT = [OPEN, CLOSE]
    TOKENS = PUNCT + [IMP]


class LinearLogicParser(LogicParser):
    

    def __init__(self):
        LogicParser.__init__(self)

        self.operator_precedence = {APP: 1, Tokens.IMP: 2, None: 3}
        self.right_associated_operations += [Tokens.IMP]

    def get_all_symbols(self):
        return Tokens.TOKENS

    def handle(self, tok, context):
        if tok not in Tokens.TOKENS:
            return self.handle_variable(tok, context)
        elif tok == Tokens.OPEN:
            return self.handle_open(tok, context)

    def get_BooleanExpression_factory(self, tok):
        if tok == Tokens.IMP:
            return ImpExpression
        else:
            return None

    def make_BooleanExpression(self, factory, first, second):
        return factory(first, second)

    def attempt_ApplicationExpression(self, expression, context):
        
        if self.has_priority(APP, context):
            if self.inRange(0) and self.token(0) == Tokens.OPEN:
                self.token()  
                argument = self.process_next_expression(APP)
                self.assertNextToken(Tokens.CLOSE)
                expression = ApplicationExpression(expression, argument, None)
        return expression

    def make_VariableExpression(self, name):
        if name[0].isupper():
            return VariableExpression(name)
        else:
            return ConstantExpression(name)


class Expression:

    _linear_logic_parser = LinearLogicParser()

    @classmethod
    def fromstring(cls, s):
        return cls._linear_logic_parser.parse(s)

    def applyto(self, other, other_indices=None):
        return ApplicationExpression(self, other, other_indices)

    def __call__(self, other):
        return self.applyto(other)

    def __repr__(self):
        return f"<{self.__class__.__name__} {self}>"


class AtomicExpression(Expression):
    def __init__(self, name, dependencies=None):
        
        assert isinstance(name, str)
        self.name = name

        if not dependencies:
            dependencies = []
        self.dependencies = dependencies

    def simplify(self, bindings=None):
        
        if bindings and self in bindings:
            return bindings[self]
        else:
            return self

    def compile_pos(self, index_counter, glueFormulaFactory):
        
        self.dependencies = []
        return (self, [])

    def compile_neg(self, index_counter, glueFormulaFactory):
        
        self.dependencies = []
        return (self, [])

    def initialize_labels(self, fstruct):
        self.name = fstruct.initialize_label(self.name.lower())

    def __eq__(self, other):
        return self.__class__ == other.__class__ and self.name == other.name

    def __ne__(self, other):
        return not self == other

    def __str__(self):
        accum = self.name
        if self.dependencies:
            accum += "%s" % self.dependencies
        return accum

    def __hash__(self):
        return hash(self.name)


class ConstantExpression(AtomicExpression):
    def unify(self, other, bindings):
        
        assert isinstance(other, Expression)
        if isinstance(other, VariableExpression):
            try:
                return bindings + BindingDict([(other, self)])
            except VariableBindingException:
                pass
        elif self == other:
            return bindings
        raise UnificationException(self, other, bindings)


class VariableExpression(AtomicExpression):
    def unify(self, other, bindings):
        
        assert isinstance(other, Expression)
        try:
            if self == other:
                return bindings
            else:
                return bindings + BindingDict([(self, other)])
        except VariableBindingException as e:
            raise UnificationException(self, other, bindings) from e


class ImpExpression(Expression):
    def __init__(self, antecedent, consequent):
        
        assert isinstance(antecedent, Expression)
        assert isinstance(consequent, Expression)
        self.antecedent = antecedent
        self.consequent = consequent

    def simplify(self, bindings=None):
        return self.__class__(
            self.antecedent.simplify(bindings), self.consequent.simplify(bindings)
        )

    def unify(self, other, bindings):
        
        assert isinstance(other, ImpExpression)
        try:
            return (
                bindings
                + self.antecedent.unify(other.antecedent, bindings)
                + self.consequent.unify(other.consequent, bindings)
            )
        except VariableBindingException as e:
            raise UnificationException(self, other, bindings) from e

    def compile_pos(self, index_counter, glueFormulaFactory):
        
        (a, a_new) = self.antecedent.compile_neg(index_counter, glueFormulaFactory)
        (c, c_new) = self.consequent.compile_pos(index_counter, glueFormulaFactory)
        return (ImpExpression(a, c), a_new + c_new)

    def compile_neg(self, index_counter, glueFormulaFactory):
        
        (a, a_new) = self.antecedent.compile_pos(index_counter, glueFormulaFactory)
        (c, c_new) = self.consequent.compile_neg(index_counter, glueFormulaFactory)
        fresh_index = index_counter.get()
        c.dependencies.append(fresh_index)
        new_v = glueFormulaFactory("v%s" % fresh_index, a, {fresh_index})
        return (c, a_new + c_new + [new_v])

    def initialize_labels(self, fstruct):
        self.antecedent.initialize_labels(fstruct)
        self.consequent.initialize_labels(fstruct)

    def __eq__(self, other):
        return (
            self.__class__ == other.__class__
            and self.antecedent == other.antecedent
            and self.consequent == other.consequent
        )

    def __ne__(self, other):
        return not self == other

    def __str__(self):
        return "{}{} {} {}{}".format(
            Tokens.OPEN,
            self.antecedent,
            Tokens.IMP,
            self.consequent,
            Tokens.CLOSE,
        )

    def __hash__(self):
        return hash(f"{hash(self.antecedent)}{Tokens.IMP}{hash(self.consequent)}")


class ApplicationExpression(Expression):
    def __init__(self, function, argument, argument_indices=None):
        
        function_simp = function.simplify()
        argument_simp = argument.simplify()

        assert isinstance(function_simp, ImpExpression)
        assert isinstance(argument_simp, Expression)

        bindings = BindingDict()

        try:
            if isinstance(function, ApplicationExpression):
                bindings += function.bindings
            if isinstance(argument, ApplicationExpression):
                bindings += argument.bindings
            bindings += function_simp.antecedent.unify(argument_simp, bindings)
        except UnificationException as e:
            raise LinearLogicApplicationException(
                f"Cannot apply {function_simp} to {argument_simp}. {e}"
            ) from e

        
        if argument_indices:
            
            if not set(function_simp.antecedent.dependencies) < argument_indices:
                raise LinearLogicApplicationException(
                    "Dependencies unfulfilled when attempting to apply Linear Logic formula %s to %s"
                    % (function_simp, argument_simp)
                )
            if set(function_simp.antecedent.dependencies) == argument_indices:
                raise LinearLogicApplicationException(
                    "Dependencies not a proper subset of indices when attempting to apply Linear Logic formula %s to %s"
                    % (function_simp, argument_simp)
                )

        self.function = function
        self.argument = argument
        self.bindings = bindings

    def simplify(self, bindings=None):
        
        if not bindings:
            bindings = self.bindings

        return self.function.simplify(bindings).consequent

    def __eq__(self, other):
        return (
            self.__class__ == other.__class__
            and self.function == other.function
            and self.argument == other.argument
        )

    def __ne__(self, other):
        return not self == other

    def __str__(self):
        return "%s" % self.function + Tokens.OPEN + "%s" % self.argument + Tokens.CLOSE

    def __hash__(self):
        return hash(f"{hash(self.antecedent)}{Tokens.OPEN}{hash(self.consequent)}")


class BindingDict:
    def __init__(self, bindings=None):
        
        self.d = {}

        if isinstance(bindings, dict):
            bindings = bindings.items()

        if bindings:
            for (v, b) in bindings:
                self[v] = b

    def __setitem__(self, variable, binding):
        
        assert isinstance(variable, VariableExpression)
        assert isinstance(binding, Expression)

        assert variable != binding

        existing = self.d.get(variable, None)

        if not existing or binding == existing:
            self.d[variable] = binding
        else:
            raise VariableBindingException(
                "Variable %s already bound to another value" % (variable)
            )

    def __getitem__(self, variable):
        
        assert isinstance(variable, VariableExpression)

        intermediate = self.d[variable]
        while intermediate:
            try:
                intermediate = self.d[intermediate]
            except KeyError:
                return intermediate

    def __contains__(self, item):
        return item in self.d

    def __add__(self, other):
        
        try:
            combined = BindingDict()
            for v in self.d:
                combined[v] = self.d[v]
            for v in other.d:
                combined[v] = other.d[v]
            return combined
        except VariableBindingException as e:
            raise VariableBindingException(
                "Attempting to add two contradicting"
                " VariableBindingsLists: %s, %s" % (self, other)
            ) from e

    def __ne__(self, other):
        return not self == other

    def __eq__(self, other):
        if not isinstance(other, BindingDict):
            raise TypeError
        return self.d == other.d

    def __str__(self):
        return "{" + ", ".join(f"{v}: {self.d[v]}" for v in sorted(self.d.keys())) + "}"

    def __repr__(self):
        return "BindingDict: %s" % self


class VariableBindingException(Exception):
    pass


class UnificationException(Exception):
    def __init__(self, a, b, bindings):
        Exception.__init__(self, f"Cannot unify {a} with {b} given {bindings}")


class LinearLogicApplicationException(Exception):
    pass


def demo():
    lexpr = Expression.fromstring

    print(lexpr(r"f"))
    print(lexpr(r"(g -o f)"))
    print(lexpr(r"((g -o G) -o G)"))
    print(lexpr(r"g -o h -o f"))
    print(lexpr(r"(g -o f)(g)").simplify())
    print(lexpr(r"(H -o f)(g)").simplify())
    print(lexpr(r"((g -o G) -o G)((g -o f))").simplify())
    print(lexpr(r"(H -o H)((g -o f))").simplify())


if __name__ == "__main__":
    demo()