predicates.functions module¶
Syntactic conversion of predicatelogic 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.

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
 Returns
A function name
function
such thatfunction_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 ifx1
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
 Returns
A model
model
with the given function names such thatreplace_functions_with_relations_in_model
(
model
)
is the given model, orNone
if no such model exists.

predicates.functions.
_compile_term
(term)¶ Syntactically compiles the given term into a list of singlefunction invocation steps.
 Parameters
term (
Term
) – term to compile, whose root is a function invocation, and which contains no variable names starting withz
. Return type
 Returns
A list of steps, each of which is a formula of the form
'
y
=
f
(
x1
,
…,
xn
)'
, wherey
is a new variable name obtained by callingnext
(
fresh_variable_name_generator
)
,f
is a function name, and each of thex
i
is either a constant name or a variable name. Ifx
i
is a new variable name, then it is also the lefthand side of a previous step, where all of the steps “leading up to”x1
precede those “leading up” tox2
, etc. If all the returned steps hold in any model, then the lefthandside 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 “oneway 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 withz
, and such that there exist no canonically corresponding function name and relation name that are both invoked in this formula. Return type
 Returns
A formula such that the given formula holds in any model
model
if and only if the returned formula holds inreplace_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 “twoway 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.
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 withz
, and such that there exist no canonically corresponding function name and relation name that are both invoked in these formulas. Return type
 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 inreplace_functions_with_relations_in_model
(
model
)
.The returned formulas hold in a model
model
if and only ifreplace_relations_with_functions_in_model
(
model
,
original_functions
)
, whereoriginal_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 for the returned formulas, the meaning 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 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
 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 elementx
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 forreplace_equality_with_SAME
(
formulas
)
. The universe of the returned model corresponds to the equivalence classes of the'SAME'
relation in the given model.