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 meanings, replacing each function meaning with a canonically corresponding relation meaning.

Parameters

model (Model[~T]) – model to convert, such that there exist no canonically corresponding function name and relation name that both have meanings in this model.

Return type

Model[~T]

Returns

A model obtained from the given model by replacing every function meaning of a function name with a relation meaning of the canonically corresponding relation name, such that the relation meaning contains any tuple (x1,,xn) if and only if x1 is the output of the function meaning for the arguments (x2,,xn).

predicates.functions.replace_relations_with_functions_in_model(model, original_functions)

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

Parameters
  • model (Model[~T]) – model to convert, that contains no function meanings.

  • 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 a meaning 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 starting with z.

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

Parameters

formula (Formula) – formula to convert, which contains no variable names starting with z, 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:

  1. The former holds in a model if and only if the latter holds in the canonically corresponding model with no function meanings.

  2. The latter holds in a model if and only if that model has a canonically corresponding model with meanings for the functions of the former, and the former holds in that model.

Parameters

formulas (AbstractSet[Formula]) – formulas to convert, which contain no variable names starting with z, 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:

  1. The given formulas hold in a model model if and only if the returned formulas hold in replace_functions_with_relations_in_model(model).

  2. 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:

  1. A formula for each of the given formulas, where each equality is replaced with a matching invocation of the relation name 'SAME'.

  2. Formula(s) that ensure that in any model for the returned formulas, the meaning of the relation name 'SAME' is reflexive, symmetric, and transitive.

  3. For each relation name from the given formulas, formula(s) that ensure that in any model for the returned formulas, the meaning of this relation name respects the meaning 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 a meaning for 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 meaning for the relation name 'SAME', to add the meaning to.

Return type

Model[~T]

Returns

A model obtained from the given model by adding a meaning for 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 meaning 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 meanings, and contains a meaning for the relation name 'SAME' that is reflexive, symmetric, transitive, and respected by the meanings of all other relation names.

Return type

Model[~T]

Returns

A model that is a model for any set formulas if and only if the given model is a model for replace_equality_with_SAME(formulas). The universe of the returned model corresponds to the equivalence classes of the 'SAME' relation in the given model.