predicates.functions module¶

Syntactic conversion of predicate-logic formulas to not use functions and equality.

predicates.functions.function_name_to_relation_name(function)¶

Converts the given function name to a canonically corresponding relation name.

Parameters: function (str) – function name to convert.
Return type: str
Returns: A relation name that is the same as the given function name, except that its first letter is capitalized.

predicates.functions.relation_name_to_function_name(relation)¶

Converts the given relation name to a canonically corresponding function name.

Parameters: relation (str) – relation name to convert.
Return type: str
Returns: A function name function such that function_name_to_relation_name(function) is the given relation name.

predicates.functions.replace_functions_with_relations_in_model(model)¶

Converts the given model to a canonically corresponding model without any function interpretations, replacing each function interpretation with a canonically corresponding relation interpretation.

Parameters: model (Model[~T]) – model to convert, such that there exist no canonically corresponding function name and relation name that both have interpretations in this model.
Return type: Model[~T]
Returns: A model obtained from the given model by replacing every function interpretation of a function name with a relation interpretation of the canonically corresponding relation name, such that the relation interpretation contains any tuple (x1,…,xn) if and only if x1 is the output of the function interpretation for the arguments (x2,…,xn).

predicates.functions.replace_relations_with_functions_in_model(model, original_functions)¶

Converts the given model with no function interpretations to a canonically corresponding model with interpretations for the given function names, having each new function interpretation replace a canonically corresponding relation interpretation.

Parameters

model (Model[~T]) – model to convert, that contains no function interpretations.
original_functions (AbstractSet[str]) – function names for the model to convert to, such that no relation name that canonically corresponds to any of these function names has an interpretation in the given model.

Return type

Optional[Model[~T]]

Returns

A model model with the given function names such that replace_functions_with_relations_in_model(model) is the given model, or None if no such model exists.

predicates.functions._compile_term(term)¶

Syntactically compiles the given term into a list of single-function invocation steps.

Parameters: term (Term) – term to compile, whose root is a function invocation, and which contains no variable names that are z followed by a number.
Return type: List[Formula]
Returns: A list of steps, each of which is a formula of the form 'y=f(x1,…,xn)', where y is a new variable name obtained by calling next(fresh_variable_name_generator), f is a function name, and each of the xi is either a constant name or a variable name. If xi is a new variable name, then it is also the left-hand side of a previous step, where all of the steps “leading up to” x1 precede those “leading up” to x2, etc. If all the returned steps hold in any model, then the left-hand-side variable name of the last returned step evaluates in that model to the value of the given term.

predicates.functions.replace_functions_with_relations_in_formula(formula)¶

Syntactically converts the given formula to a formula that does not contain any function invocations, and is “one-way equivalent” in the sense that the former holds in a model if and only if the latter holds in the canonically corresponding model with no function interpretations.

Parameters: formula (Formula) – formula to convert, which contains no variable names that are z followed by a number, and such that there exist no canonically corresponding function name and relation name that are both invoked in this formula.
Return type: Formula
Returns: A formula such that the given formula holds in any model model if and only if the returned formula holds in replace_function_with_relations_in_model(model).

predicates.functions.replace_functions_with_relations_in_formulas(formulas)¶

Syntactically converts the given set of formulas to a set of formulas that do not contain any function invocations, and is “two-way equivalent” in the sense that:

The former holds in a model if and only if the latter holds in the canonically corresponding model with no function interpretations.
The latter holds in a model if and only if that model has a canonically corresponding model with interpretations for the functions names of the former, and the former holds in that model.

Parameters

formulas (AbstractSet[Formula]) – formulas to convert, which contain no variable names that are z followed by a number, and such that there exist no canonically corresponding function name and relation name that are both invoked in these formulas.

Return type

Set[Formula]

Returns

A set of formulas, one for each given formula as well as one additional formula for each relation name that replaces a function name from the given formulas, such that:

The given formulas hold in a model model if and only if the returned formulas hold in replace_functions_with_relations_in_model(model).
The returned formulas hold in a model model if and only if replace_relations_with_functions_in_model(model,original_functions), where original_functions are all the function names in the given formulas, is a model and the given formulas hold in it.

predicates.functions.replace_equality_with_SAME_in_formulas(formulas)¶

Syntactically converts the given set of formulas to a canonically corresponding set of formulas that do not contain any equalities, consisting of the following formulas:

A formula for each of the given formulas, where each equality is replaced with a matching invocation of the relation name 'SAME'.
Formula(s) that ensure that in any model of the returned formulas, the interpretation of the relation name 'SAME' is reflexive, symmetric, and transitive.
For each relation name from the given formulas, formula(s) that ensure that in any model of the returned formulas, the interpretation of this relation name respects the interpretation of the relation name 'SAME'.

Parameters: formulas (AbstractSet[Formula]) – formulas to convert, that contain no function names and do not contain the relation name 'SAME'.
Return type: Set[Formula]
Returns: The converted set of formulas.

predicates.functions.add_SAME_as_equality_in_model(model)¶

Adds an interpretation of the relation name 'SAME' in the given model, that canonically corresponds to equality in the given model.

Parameters: model (Model[~T]) – model that has no interpretation of the relation name 'SAME', to add the interpretation to.
Return type: Model[~T]
Returns: A model obtained from the given model by adding an interpretation of the relation name 'SAME', that contains precisely all pairs (x,x) for every element x of the universe of the given model.

predicates.functions.make_equality_as_SAME_in_model(model)¶

Converts the given model to a model where equality coincides with the interpretation of 'SAME' in the given model, in the sense that any set of formulas holds in the returned model if and only if its canonically corresponding set of formulas that do not contain equality holds in the given model.

Parameters: model (Model[~T]) – model to convert, that contains no function interpretations, and contains an interpretation of the relation name 'SAME' that is reflexive, symmetric, transitive, and respected by the interpretations of all other relation names.
Return type: Model[~T]
Returns: A model that is a model of any set formulas if and only if the given model is a model of replace_equality_with_SAME(formulas). The universe of the returned model corresponds to the equivalence classes of the interpretation of 'SAME' in the given model.