Variables, Terms, Atoms

Generic

Variables, Terms, Atoms#

Generic abstract classes specify atomic formulas, terms, and variables at the first-order level, where the syntax and semantics of the underlying theories is unknown. The classes primarily act as interfaces specifying methods that are used as black boxes within Formula methods.

Generic Types#

We use type variables atomic.α, atomic.τ, and atomic.χ with the same names and definitions as in module formula.

logic1.firstorder.atomic.α = TypeVar('α', bound='AtomicFormula')#: A type variable denoting a type of atomic formulas with upper bound logic1.firstorder.atomic.AtomicFormula.

logic1.firstorder.atomic.τ = TypeVar('τ', bound='Term')#: A type variable denoting a type of terms with upper bound logic1.firstorder.atomic.Term.

logic1.firstorder.atomic.χ = TypeVar('χ', bound='Variable')#: A type variable denoting a type of variables with upper bound logic1.firstorder.atomic.Variable.

logic1.firstorder.atomic.σ = TypeVar('σ')#: A type variable denoting a type that is admissible in addition to terms as a dictionary entry in AtomicFormula.subs(). Instances of type σ that are passed to AtomicFormula.subs() must not contain any variables. A typical example is setting σ to int in the theory of real closed fields.

Set of Variables#

class logic1.firstorder.atomic.VariableSet[source]#

Bases: Generic[χ]

The infinite set of all variables of a theory. Variables are uniquely identified by their name, which is a str. Subclasses within theories are singletons, and their unique instance is assigned to a module variable VV there.

See also

Derived classes in various theories and their unique instances: RCF.atomic.VariableSet, RCF.atomic.VV for Real Closed Fields and Sets.atomic.VariableSet, Sets.atomic.VV for Sets.

abstract __getitem__(index: str) → χ[source]#

Obtain the unique variable with name index.

>>> from logic1.theories import RCF
>>> assert isinstance(RCF.VV, RCF.atomic.VariableSet)
>>> x = RCF.VV['x']; x
x
>>> assert isinstance(x, RCF.atomic.Variable)

See also

get() – obtain several variables simultaneously
imp() – import variables into global namespace

final get(*args: str) → tuple[χ, ...][source]#

Obtain several variables simultaneously by their names.

>>> from logic1.theories import RCF
>>> assert isinstance(RCF.VV, RCF.atomic.VariableSet)
>>> x, y = RCF.VV.get('x', 'y')
>>> assert isinstance(x, RCF.atomic.Variable)
>>> assert isinstance(y, RCF.atomic.Variable)

See also

__getitem__() – obtain variable by its name
imp() – import variables into global namespace

final imp(*args: str) → None[source]#

Import variables into global namespace. This works only interactively, i.e., if __name__ == '__main__'. Otherwise use get().

>>> if __name__ == '__main__':  # to prevent doctest failure
...     from logic1.theories import RCF
...     assert isinstance(RCF.VV, RCF.atomic.VariableSet)
...     RCF.VV.imp('x', 'y')
...     assert isinstance(x, RCF.atomic.Variable)
...     assert isinstance(y, RCF.atomic.Variable)

See also

__getitem__() – obtain variable by its name
get() – obtain several variables simultaneously

abstract pop() → None[source]#

abstract push() → None[source]#

push() pushes the current status regarding used variables to a private stack and resets to the initial state where all variables are marked as unused. pop() recovers the status from the stack and thereby overwrites the current status.

Attention

stack, push(), and pop() are reserved for special situations.

They allow to obtain variables from fresh() within asychronous doctests in a reproducable way. In the following example, Formula.to_pnf() indirectly uses RCF.atomic.VariableSet.fresh():

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> x, a = VV.get('x', 'a')
>>> f = And(x == 0, Ex(x, x == a))
>>> f.to_pnf()
Ex(G0001_x, And(x == 0, -G0001_x + a == 0))
>>> f.to_pnf()
Ex(G0002_x, And(x == 0, -G0002_x + a == 0))
>>> VV.push()
>>> x, a = VV.get('x', 'a')
>>> g = And(x == 0, Ex(x, x == a))
>>> g.to_pnf()
Ex(G0001_x, And(x == 0, -G0001_x + a == 0))
>>> VV.pop()
>>> f.to_pnf()
Ex(G0003_x, And(x == 0, -G0003_x + a == 0))

Notice that we are not using any previously existing variables between VV.push() and VV.pop() above.

See logic1/theories/RCF/test_pnf.txt for a complete doctest file using this approach

Terms#

class logic1.firstorder.atomic.Term[source]#

Bases: Generic[τ, χ, σ]

This abstract class specifies an interface via the definition of abstract methods on terms required by Formula. The methods are supposed to be implemented for the various theories. We need a type variable <.firstorder.atomic.τ>` for this class itself, because Self cannot be used in the static method sort_key().

See also

Derived classes in various theories: RCF.atomic.Term for Real Closed Fields.

Note

The theory logic1.theories.Sets does not subclass Term. Since it has no function symbols, it can use instances of Sets.atomic.Variable as terms.

abstract as_latex() → str[source]#: LaTeX representation as a string. This is required by Formula.as_latex() for the representation of quantified variables.

abstract static sort_key(term: τ) → Any[source]#

A sort key suitable for ordering instances of τ.

Note

We reserve Python’s rich comparisons __lt__, __le__ etc. as constructors for instances of subclasses of AtomicFormula. For example, RCF.atomic.Term.__lt__ constructs an inequality

>>> from logic1.theories.RCF import *
>>> a, b = VV.get('a', 'b')
>>> a < b
a - b < 0
>>> type(_)
<class 'logic1.theories.RCF.atomic.Lt'>

As a consquence, rich comparisons are not available for defining an ordering on terms, and we instead provid a key, which can be used, e.g., with Python’s sorted, or directly as follows:

>>> Term.sort_key(a) < Term.sort_key(b)
False
>>> sorted([a, b], key=Term.sort_key)
[b, a]

In contrast, atomic formulas and, more generally, formulas support rich comparisons.

abstract vars() → Iterator[χ][source]#

An iterator over all occurring variables. Each occurring variable is reported once.

See also

Formula.bvars() – all occurring bound variables
Formula.fvars() – all occurring free variables
Formula.qvars() – all quantified variables

Variables#

class logic1.firstorder.atomic.Variable[source]#

Bases: Term[χ, χ, σ]

This abstract class specifies an interface via the definition of abstract methods on variables required by Formula. The methods are supposed to be implemented for the various theories.

See also

Derived classes in various theories: RCF.atomic.Variable for Real Closed Fields and Sets.atomic.Variable for Sets.

abstract fresh() → χ[source]#: Returns a variable that has not been used so far.

Atomic Formulas#

class logic1.firstorder.atomic.AtomicFormula[source]#

Bases: Formula[α, τ, χ, σ]

This abstract class primarily specifies an interface via the definition of abstract methods on atomic formulas that are required by Formula. In addition, it provides some final implementations of such methods, where they do not depend on the syntax or sematic of the specific theory.

See also

Derived classes in various theories: RCF.atomic.AtomicFormula for Real Closed Fields and Sets.atomic.AtomicFormula for Sets.

abstract __le__(other: Formula[α, τ, χ, σ]) → bool[source]#: Returns True if self should be sorted before or is equal to other. This method is required by the corresponding first-order method Formula.__le__().

abstract __str__() → str[source]#: Representation of this atomic formula used in printing. This method is required by the corresponding recursive first-order method.

abstract as_latex() → str[source]#: Latex representation as a string. This method is required by the corresponding recursive first-order method Formula.as_latex().

abstract bvars(quantified: frozenset[χ] = frozenset({})) → Iterator[χ][source]#: Iterate over occurrences of variables that are elements of quantified. Yield each such variable once for each term that it occurs in. This method is required by the corresponding recursive first-order method Formula.bvars().

abstract classmethod complement() → type[α][source]#

The complement operator of an atomic formula, i.e., a.complement(*a.args) is an atomic formula equivalent to Not(a.op(*a.args)).

See also

to_complement() – generalization from relations to atomic formulas

abstract fvars(quantified: frozenset[χ] = frozenset({})) → Iterator[χ][source]#: Iterate over occurrences of variables that are not elements of quantified. Yield each such variable once for each term that it occurs in. This method is required by the corresponding recursive first-order method Formula.fvars().

abstract simplify() → Formula[α, τ, χ, σ][source]#: Fast basic simplification. The result is equivalent to self. This method is required by the corresponding recursive first-order method Formula.simplify().

abstract subs(substitution: dict[χ, τ | σ]) → α[source]#: Simultaneous substitution of terms from τ or constants from σ for variables from χ. This method is required by the corresponding recursive first-order method Formula.subs().

final to_complement() → α[source]#: Returns an AtomicFormula equivalent to Not(self).

See also

complement – complement relation

Variables, Terms, Atoms

Contents

Variables, Terms, Atoms#

Generic Types#

Set of Variables#

Terms#

Variables#

Atomic Formulas#