Source code for logic1.firstorder.formula

from __future__ import annotations

from abc import abstractmethod
import functools
from typing import Any, Callable, Final, Generic, Iterable, Iterator, Self, TypeVar
from typing_extensions import TypeIs

from ..support.tracing import trace  # noqa


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

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

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

σ = TypeVar('σ')
"""A type variable denoting a type admissible as a dictionary entry in
:meth:`.subs`, in addition to terms. Instances of type :data:`.σ` that are
passed to :meth:`.subs` must not contain any variables. A typical example
is :data:`σ` == :class:`int` in the theory of real closed fields.
"""


[docs] @functools.total_ordering class Formula(Generic[α, τ, χ, σ]): r"""This abstract base class implements representations of and methods on first-order formulas recursively built using first-order operators: 1. Boolean operators: a. Truth values :math:`\top` and :math:`\bot` b. Negation :math:`\lnot` c. Conjunction :math:`\land` and discjunction :math:`\lor` d. Implication :math:`\longrightarrow` e. Bi-implication (syntactic equivalence) :math:`\longleftrightarrow` 2. Quantifiers :math:`\exists x` and :math:`\forall x`, where :math:`x` is a variable. As an abstract base class, :class:`Formula` cannot be instantiated. Nevertheless, it implements a number of methods on first-order formualas. The methods implemented here are typically syntactic in the sense that they do not need to know the semantics of the underlying theories. .. note:: :class:`Formula` depends on three type variables :data:`.α`, :data:`.τ`, :data:`.χ` for the types ocurring atomic formula, terms, and variables, respectively. They appear in type annotations used by static type checkers but are not relevant for the either interactive use or use as a library. """ @property def op(self) -> type[Self]: """Operator. This property can be used with instances of subclasses of :class:`Formula`. It yields the respective subclass. """ return type(self) @property def args(self) -> tuple[Any, ...]: """The arguments of a formula as a tuple. .. seealso:: * :attr:`Equivalent.lhs <.boolean.Equivalent.lhs>` \ -- left hand side of a logical :math:`\\longleftrightarrow` * :attr:`Equivalent.rhs <.boolean.Equivalent.lhs>` \ -- right hand side of a logical :math:`\\longleftrightarrow` * :attr:`Implies.lhs <.boolean.Equivalent.lhs>` \ -- left hand side of a logical :math:`\\longrightarrow` * :attr:`Implies.rhs <.boolean.Equivalent.lhs>` \ -- right hand side of a logical :math:`\\longrightarrow` * :attr:`Not.arg <.boolean.Not.arg>` \ -- argument formula of a logical :math:`\\neg` * :attr:`QuantifiedFormula.arg <.quantified.QuantifiedFormula.arg>` \ -- argument formula of a quantifier :math:`\\exists` or \ :math:`\\forall` * :attr:`QuantifiedFormula.var <.quantified.QuantifiedFormula.var>` \ -- variable of a quantifier :math:`\\exists` or :math:`\\forall` """ return self._args @args.setter def args(self, args: tuple[Any, ...]) -> None: self._args = args
[docs] def __and__(self, other: Formula[α, τ, χ, σ]) -> Formula[α, τ, χ, σ]: """Override the :obj:`& <object.__and__>` operator to apply :class:`.boolean.And`. >>> from logic1.theories.RCF import Eq >>> >>> Eq(0, 0) & Eq(1 + 1, 2) & Eq(1 + 1 + 1, 3) And(Eq(0, 0), Eq(2, 2), Eq(3, 3)) """ return And(self, other)
def __eq__(self, other: object) -> bool: """A recursive test for equality of the `self` and `other`. Note that this is not a logical operator for equality. >>> from logic1.theories.RCF import Ne >>> >>> e1 = Ne(1, 0) >>> e2 = Ne(1, 0) >>> e1 == e2 True >>> e1 is e2 False """ if self is other: return True if not isinstance(other, Formula): return NotImplemented return self.op == other.op and self.args == other.args def __getnewargs__(self) -> tuple[Any, ...]: return self.args def __hash__(self) -> int: """ Hash function. hash() yields deterministic results for a fixed hash seed. Set the environment variable PYTHONHASHSEED to a positive integer when comparing hashes from various Python sessions, e.g. for debugging. Recall from the Python documentation that PYTHONHASHSEED should not be fixed in general. """ return hash((tuple(str(cls) for cls in self.op.mro()), self.args))
[docs] @abstractmethod def __init__(self, *args: object) -> None: """This abstract base class is not supposed to have instances itself. Technically this is enforced via this abstract initializer. """ ...
[docs] def __invert__(self) -> Formula[α, τ, χ, σ]: """Override the :obj:`~ <object.__invert__>` operator to apply :class:`Not`. >>> from logic1.theories.RCF import VV >>> x, = VV.get('x') >>> ~ (x == 0) Not(x == 0) """ return Not(self)
[docs] def __le__(self, other: Formula[α, τ, χ, σ]) -> bool: """Returns :external:obj:`True` if `self` should be sorted before or is equal to other. .. seealso:: * :meth:`AtomicFormula.__le__() <.firstorder.atomic.AtomicFormula.__le__>`\ -- comparison of atomic formulas """ L = (And, Or, Not, Implies, Equivalent, Ex, All, _T, _F) # The case "self: AtomicFormula" is caught by the implementation of the # abstract method AtomicFormula.__le__: assert isinstance(self, L) if isinstance(other, L): if self.op != other.op: return L.index(self.op) < L.index(other.op) return self.args <= other.args # The following is a milder reference to AtomicFormula than the # original code: assert isinstance(other, AtomicFormula) return False
[docs] def __lshift__(self, other: Formula[α, τ, χ, σ]) -> Formula[α, τ, χ, σ]: r"""Override the :obj:`\<\< <object.__lshift__>` operator to apply :class:`Implies` with reversed sides. >>> from logic1.theories.RCF import Eq, VV >>> x, y, z = VV.get('x', 'y', 'z') >>> >>> (x + z == y + z) << (x == y) Implies(x - y == 0, x - y == 0) """ return Implies(other, self)
def __ne__(self, other: object) -> bool: """A recursive test for unequality of the `self` and `other`. """ return not self == other
[docs] def __or__(self, other: Formula[α, τ, χ, σ]) -> Formula[α, τ, χ, σ]: """Override the :obj:`| <object.__or__>` operator to apply :class:`Or`. >>> from logic1.theories.RCF import * >>> x, y, z = VV.get('x', 'y', 'z') >>> >>> (x == 0) | (x == y) | (x == z) Or(x == 0, x - y == 0, x - z == 0) """ return Or(self, other)
def __repr__(self) -> str: """A Representation of the :class:`Formula` `self` that is suitable for use as an input. """ r = self.op.__name__ r += '(' if self.args: r += self.args[0].__repr__() for a in self.args[1:]: r += ', ' + a.__repr__() r += ')' return r
[docs] def __rshift__(self, other: Formula[α, τ, χ, σ]) -> Formula[α, τ, χ, σ]: """Override the :obj:`>> <object.__rshift__>` operator to apply :class:`Implies`. >>> from logic1.theories.RCF import * >>> x, y, z = VV.get('x', 'y', 'z') >>> >>> (x == y) >> (x + z == y + z) Implies(x - y == 0, x - y == 0) """ return Implies(self, other)
[docs] def __str__(self) -> str: """Representation of the Formula used in printing. """ SYMBOL: Final = { All: 'All', Ex: 'Ex', And: 'and', Or: 'or', Implies: '-->', Equivalent: '<-->', Not: 'not', _F: 'F', _T: 'T'} PRECEDENCE: Final = { All: 99, Ex: 99, And: 50, Or: 50, Implies: 10, Equivalent: 10, Not: 99, _F: 99, _T: 99} SPACING: Final = ' ' match self: case All() | Ex(): L = [] arg: Formula = self while isinstance(arg, (All, Ex)) and arg.op == self.op: L.append(arg.var) arg = arg.arg variables = tuple(L) if len(L) > 1 else L[0] return f'{SYMBOL[self.op]}({variables}, {arg})' case And() | Or() | Equivalent() | Implies(): L = [] for arg in self.args: arg_as_str = str(arg) if PRECEDENCE[self.op] >= PRECEDENCE.get(arg.op, 100): arg_as_str = f'({arg_as_str})' L.append(arg_as_str) return f'{SPACING}{SYMBOL[self.op]}{SPACING}'.join(L) case Not(): arg_as_str = str(self.arg) if self.arg.op not in (Ex, All, Not): arg_as_str = f'({arg_as_str})' return f'{SYMBOL[Not]}{SPACING}{arg_as_str}' case _F() | _T(): return SYMBOL[self.op] case _: # Atomic formulas are caught by the implementation of the # abstract method AtomicFormula.__str__. assert False, repr(self)
[docs] def all(self, ignore: Iterable[χ] = set()) -> Formula[α, τ, χ, σ]: """Universal closure. Universally quantifiy all variables occurring free in `self`, except the ones in `ignore`. >>> from logic1.theories.RCF import * >>> a, b, x = VV.get('a', 'b', 'x') >>> f = Ex(x, And(x >= 0, a*x + b == 0)) >>> f.all() All(b, All(a, Ex(x, And(x >= 0, a*x + b == 0)))) .. seealso:: * :class:`All <.quantified.All>` -- universal quantifier * :meth:`ex` -- existential closure * :meth:`quantify` -- add quantifier prefix """ variables = list(set(self.fvars()) - set(ignore)) if variables: variables.sort(key=variables[0].sort_key) f = self for v in reversed(variables): f = All(v, f) return f
[docs] def as_latex(self) -> str: r"""LaTeX representation as a string, which can be used elsewhere. >>> from logic1.theories.RCF import * >>> x, y = VV.get('x', 'y') >>> f = All(x, Or(x < 1, x - 1 == 0, x > 1)) >>> f.as_latex() '\\forall x \\, (x - 1 < 0 \\, \\vee \\, x - 1 = 0 \\, \\vee \\, x - 1 > 0)' .. seealso:: :meth:`_repr_latex_` -- LaTeX representation for Jupyter notebooks """ SYMBOL: Final = { All: '\\forall', Ex: '\\exists', And: '\\wedge', Or: '\\vee', Implies: '\\longrightarrow', Equivalent: '\\longleftrightarrow', Not: '\\neg', _F: '\\bot', _T: '\\top'} PRECEDENCE: Final = { All: 99, Ex: 99, And: 50, Or: 50, Equivalent: 10, Implies: 10, Not: 99, _F: 99, _T: 99} SPACING: Final = ' \\, ' match self: case All() | Ex(): var_as_latex = self.var.as_latex() arg_as_latex = self.arg.as_latex() if self.arg.op not in (Ex, All, Not): arg_as_latex = f'({arg_as_latex})' return f'{SYMBOL[self.op]} {var_as_latex}{SPACING}{arg_as_latex}' case And() | Or() | Equivalent() | Implies(): L = [] for arg in self.args: arg_as_latex = arg.as_latex() if PRECEDENCE[self.op] >= PRECEDENCE.get(arg.op, 99): arg_as_latex = f'({arg_as_latex})' L.append(arg_as_latex) return f'{SPACING}{SYMBOL[self.op]}{SPACING}'.join(L) case Not(): arg_as_latex = self.arg.as_latex() if self.arg.op not in (Ex, All, Not): arg_as_latex = f'({arg_as_latex})' return f'{SYMBOL[Not]}{SPACING}{arg_as_latex}' case _F() | _T(): return SYMBOL[self.op] case _: # Atomic formulas are caught by the implementation of the # abstract method AtomicFormula.as_latex. assert False
[docs] def atoms(self) -> Iterator[α]: """ An iterator over all instances of :class:`AtomicFormula <.firstorder.atomic.AtomicFormula>` occurring in `self`. Recall that the truth values :data:`T <.boolean.T>` and :data:`F <.boolean.F>` are not atoms: >>> from logic1.theories.RCF import * >>> x, y, z = VV.get('x', 'y', 'z') >>> f = Or(And(x == 0, y == 0, T), And(x == 0, y == z, z != 0)) >>> list(f.atoms()) [x == 0, y == 0, x == 0, y - z == 0, z != 0] The overall number of atoms: >>> sum(1 for _ in f.atoms()) 5 Count numbers of occurrences for each occurring atom using a :external+python:class:`Counter <collections.Counter>`: >>> from collections import Counter >>> Counter(f.atoms()) Counter({x == 0: 2, y == 0: 1, y - z == 0: 1, z != 0: 1}) Recall the Python builtin :func:`next`: >>> iter = (x == 0).atoms() >>> next(iter) x == 0 >>> next(iter) Traceback (most recent call last): ... StopIteration """ match self: case All() | Ex(): yield from self.arg.atoms() case And() | Or() | Not() | Implies() | Equivalent() | _F() | _T(): for arg in self.args: yield from arg.atoms() case _: # Atomic formulas are caught by the final method # AtomicFormula.atoms. assert False, type(self)
[docs] def bvars(self, quantified: frozenset[χ] = frozenset()) -> Iterator[χ]: """An iterator over all bound occurrences of variables in `self`. Each variable is reported once for each term that it occurs in. >>> from logic1.theories.RCF import * >>> a, x, y, z = VV.get('a', 'x', 'y', 'z') >>> f = All(y, And(Ex(x, a + x == y), Ex(z, x + y == a + x))) >>> list(f.bvars()) [x, y, y] Note that following the common definition in logic, *occurrence* refers to the occurrence in a term. Appearances of variables as a quantified variables without use in any term are not considered. The parameter `quantified` specifies variable to be considered bound in addition to those that are explicitly quantified in `self`. .. seealso:: * :meth:`fvars` -- all occurring free variables * :meth:`qvars` -- all quantified variables * :meth:`Term.vars() <.firstorder.atomic.Term.vars>` -- all occurring variables """ match self: case All() | Ex(): yield from self.arg.bvars(quantified.union({self.var})) case And() | Or() | Not() | Implies() | Equivalent() | _F() | _T(): for arg in self.args: yield from arg.bvars(quantified) case _: assert False, type(self)
[docs] def count_alternations(self) -> int: """Count the number of quantifier alternations. Returns the maximal number of quantifier alternations along a path from the root to a leaf of the expression tree. Occurrence of quantified variables is not checked, so that quantifiers with unused variables are counted. >>> from logic1.theories import RCF >>> x, y, z = RCF.VV.get('x', 'y', 'z') >>> f = Ex(x, (x == y) & All(x, Ex(y, Ex(z, x == x + 1)))) >>> f.count_alternations() 2 In this example the following path has two alternations, one from :class:`Ex <.quantified.Ex>` to :class:`All <.quantified.All>` and another one from :class:`All <.quantified.All>` to :class:`Ex <.quantified.Ex>`:: Ex ———— And ———— All ———— Ex ———— Ex ———— x == y + 1 """ return self._count_alternations()[0]
def _count_alternations(self) -> tuple[int, set[type[All | Ex]]]: match self: case All() | Ex(): count, quantifiers = self.arg._count_alternations() if self.dual() in quantifiers: return (count + 1, {self.op}) return (count, quantifiers) case And() | Or() | Not() | Implies() | Equivalent(): highest_count = -1 highest_count_quantifiers: set[type[Ex | All]] = {All, Ex} for arg in self.args: count, quantifiers = arg._count_alternations() if count > highest_count: highest_count = count highest_count_quantifiers = quantifiers elif count == highest_count: highest_count_quantifiers.update(quantifiers) return (highest_count, highest_count_quantifiers) case _F() | _T() | AtomicFormula(): # All and Ex have no annotation in the return type, because we # suspect a MyPy bug. There would be a type error here, which # disappears when introucing a variable for the return value. return (-1, {All, Ex}) case _: assert False, type(self)
[docs] def depth(self) -> int: """The depth of a formula is the maximal length of a path from the root to a truth value or an :class:`AtomicFormula <.firstorder.atomic.AtomicFormula>` in the expression tree: >>> from logic1.theories.RCF import * >>> x, y, z = VV.get('x', 'y', 'z') >>> f = Ex(x, And(x == y, All(x, Ex(y, Ex(z, x == y + 1))))) >>> f.depth() 5 In this example the the following path has the maximal length 5:: Ex ———— And ———— All ———— Ex ———— Ex ———— x == y + 1 Note that for this purpose truth values and :class:`AtomicFormula <.firstorder.atomic.AtomicFormula>` are considered to have depth 0. """ match self: case All() | Ex(): return self.arg.depth() + 1 case And() | Or() | Not() | Implies() | Equivalent(): return max(arg.depth() for arg in self.args) + 1 case _F() | _T() | AtomicFormula(): return 0 case _: assert False, type(self)
[docs] def ex(self, ignore: Iterable[χ] = set()) -> Formula[α, τ, χ, σ]: """Existential closure. Existentially quantifiy all variables occurring free in `self`, except the ones in `ignore`. >>> from logic1.theories.RCF import * >>> a, b, c, x = VV.get('a', 'b', 'c', 'x') >>> f = All(x, And(a < x, x + a - b < 0)) >>> f.ex(ignore={c}) Ex(b, Ex(a, All(x, And(a - x < 0, a - b + x < 0)))) .. seealso:: * :class:`Ex <.quantified.Ex>` -- existential quantifier * :meth:`all` -- universal closure * :meth:`quantify` -- add quantifier prefix """ variables = list(set(self.fvars()) - set(ignore)) if variables: variables.sort(key=variables[0].sort_key) f = self for v in reversed(variables): f = Ex(v, f) return f
[docs] def fvars(self, quantified: frozenset[χ] = frozenset()) -> Iterator[χ]: """An iterator over all free occurrences of variables in `self`. Each variable is reported once for each term that it occurs in. The parameter `quantified` specifies variable to be considered bound in addition to those that are explicitly quantified in `self`. >>> from logic1.theories.RCF import * >>> a, x, y, z = VV.get('a', 'x', 'y', 'z') >>> f = All(y, And(Ex(x, a + x - y == 0), Ex(z, x + y == a))) >>> list(f.fvars()) [a, a, x] .. seealso:: * :meth:`bvars` -- all occurring bound variables * :meth:`qvars` -- all quantified variables * :meth:`Term.vars() <.firstorder.atomic.Term.vars>` -- all occurring variables """ match self: case All() | Ex(): yield from self.arg.fvars(quantified.union({self.var})) case And() | Or() | Not() | Implies() | Equivalent() | _F() | _T(): for arg in self.args: yield from arg.fvars(quantified) case _: assert False, type(self)
[docs] @staticmethod def is_all(f: Formula[α, τ, χ, σ]) -> TypeIs[All[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.quantified.All`. """ return isinstance(f, All)
[docs] @staticmethod def is_and(f: Formula[α, τ, χ, σ]) -> TypeIs[And[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.boolean.And`. """ return isinstance(f, And)
[docs] @staticmethod def is_atomic(f: Formula[α, τ, χ, σ]) -> TypeIs[α]: """Type narrowing :func:`isinstance` test for :class:`.first-order.atomic.AtomicFormula`. """ return isinstance(f, AtomicFormula)
[docs] @staticmethod def is_boolean_formula(f: Formula[α, τ, χ, σ]) -> TypeIs[BooleanFormula[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.boolean.BooleanFormula`. """ return isinstance(f, BooleanFormula)
[docs] @staticmethod def is_equivalent(f: Formula[α, τ, χ, σ]) -> TypeIs[Equivalent[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.boolean.Equivalent`. """ return isinstance(f, Equivalent)
[docs] @staticmethod def is_ex(f: Formula[α, τ, χ, σ]) -> TypeIs[Ex[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.quantified.Ex`. """ return isinstance(f, Ex)
[docs] @staticmethod def is_false(f: Formula[α, τ, χ, σ]) -> TypeIs[_F[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.boolean._F`. """ return isinstance(f, _F)
[docs] @staticmethod def is_implies(f: Formula[α, τ, χ, σ]) -> TypeIs[Implies[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.boolean.Implies`. """ return isinstance(f, Implies)
[docs] @staticmethod def is_not(f: Formula[α, τ, χ, σ]) -> TypeIs[Not[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.boolean.Not`. """ return isinstance(f, Not)
[docs] @staticmethod def is_or(f: Formula[α, τ, χ, σ]) -> TypeIs[Or[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.boolean.Or`. """ return isinstance(f, Or)
[docs] @staticmethod def is_quantified_formula(f: Formula[α, τ, χ, σ]) -> TypeIs[QuantifiedFormula[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.quantified.QuantifiedFormula`. """ return isinstance(f, QuantifiedFormula)
[docs] @staticmethod def is_true(f: Formula[α, τ, χ, σ]) -> TypeIs[_T[α, τ, χ, σ]]: """Type narrowing :func:`isinstance` test for :class:`.boolean._T`. """ return isinstance(f, _T)
[docs] @staticmethod def is_term(t: τ | σ) -> TypeIs[τ]: """Type narrowing :func:`isinstance` test for :class:`.firstorder.atomic.Term`. """ return isinstance(t, Term)
[docs] def matrix(self) -> tuple[Formula[α, τ, χ, σ], Prefix[χ]]: """The matrix of a prenex formula is its quantifier free part. Its prefix is a double ended queue holding blocks of quantifiers. >>> from logic1.theories.RCF import * >>> x, y, z = VV.get('x', 'y', 'z') >>> f = All(x, All(y, Ex(z, x - y == z))) >>> m, B = f.matrix() >>> m x - y - z == 0 >>> B Prefix([(<class 'logic1.firstorder.quantified.All'>, [x, y]), (<class 'logic1.firstorder.quantified.Ex'>, [z])]) If `self` is not prenex, then the leading quantifiers are considered and the matrix will not be quantifier-free: >>> h = All(x, All(y, Implies(x != 0, Ex(z, x * z == y)))) >>> m, B = h.matrix() >>> m Implies(x != 0, Ex(z, x*z - y == 0)) >>> B Prefix([(<class 'logic1.firstorder.quantified.All'>, [x, y])]) .. seealso:: * :class:`Prefix <.quantified.Prefix>` -- a quantifier prefix * :meth:`quantify` -- add quantifier prefix * :meth:`to_pnf` -- prenex normal form """ block_vars = [] mat = self pre: Prefix[χ] = Prefix() while isinstance(mat, (Ex, All)): block_quantifier = type(mat) while isinstance(mat, block_quantifier): block_vars.append(mat.args[0]) mat = mat.args[1] pre.append((block_quantifier, block_vars)) block_vars = [] return mat, pre
[docs] def quantify(self, prefix: Prefix[χ]) -> Formula[α, τ, χ, σ]: """Add quantifier prefix. >>> from logic1.theories.RCF import * >>> x, y, z = VV.get('x', 'y', 'z') >>> f = x - y == z >>> p = Prefix((All, [x, y]), (Ex, [z])) >>> f.quantify(p) All(x, All(y, Ex(z, x - y - z == 0))) .. seealso:: * :class:`Prefix <.quantified.Prefix>` -- a quantifier prefix * :meth:`all` -- universal closure * :meth:`ex` -- existential closure * :meth:`matrix` -- prenex formula without quantifier prefix """ f = self for q, V in reversed(prefix): f = q(V, f) return f
[docs] def qvars(self) -> Iterator[χ]: """An iterator over all quantified variables in `self`. In the following example, ``z`` is a quantified variable but not a bound variable: >>> from logic1.theories.RCF import * >>> a, b, c, x, y, z = VV.get('a', 'b', 'c', 'x', 'y', 'z') >>> f = All(y, And(Ex(x, a == y), Ex(z, a == y))) >>> list(f.qvars()) [y, x, z] .. seealso:: * :meth:`bvars` -- all occurring bound variables * :meth:`fvars` -- all occurring free variables * :meth:`Term.vars() <.firstorder.atomic.Term.vars>` -- all occurring variables """ match self: case All() | Ex(): yield self.var yield from self.arg.qvars() case And() | Or() | Not() | Implies() | Equivalent() | _F() | _T(): for arg in self.args: yield from arg.qvars() case AtomicFormula(): yield from () case _: assert False, type(self)
[docs] def _repr_latex_(self) -> str: """A LaTeX representation for Jupyter notebooks. In general, the underlying method :meth:`as_latex` should be used instead. Due to a current limitation of Jupyter, the LaTeX representration is cut off after at most 5000 characters. .. seealso:: :meth:`as_latex` -- LaTeX representation """ limit = 5000 as_latex = self.as_latex() if len(as_latex) > limit: as_latex = as_latex[:limit] opc = 0 for pos in range(limit): match as_latex[pos]: case '{': opc += 1 case '}': opc -= 1 assert opc >= 0 while opc > 0: match as_latex[-1]: case '{': opc -= 1 case '}': opc += 1 as_latex = as_latex[:-1] as_latex += '{}\\dots' return f'$\\displaystyle {as_latex}$'
[docs] def simplify(self) -> Formula[α, τ, χ, σ]: """Fast basic simplification. The result is equivalent to `self`. The following first-order simplifications are applied: 1. Truth values: a. Evaluate ``Not(F)`` to ``T``, and evaluate ``Not(T)`` to ``F``. b. Evaluate ``And(..., F, ...)`` to ``F`` and ``Or(..., T, ...)`` to ``T``. c. Evaluate ``Implies(F, arg)`` and ``Implies(arg, T)`` to ``T``. d. Remove ``T`` from ``And(..., T, ...)`` and ``F`` from ``Or(..., F, ...)``. e. Transform ``Implies(T, arg)`` into ``arg``, and transform ``Implies(arg, F)`` into ``Not(arg)``. f. Transform ``Equivalent(T, arg)`` and ``Equivalent(arg, T)`` into ``arg``, and transform ``Equivalent(F, arg)``, ``Equivalent(arg, F)`` into ``Not(arg)``. 2. Nested operators: a. Transform ``Not(Not(arg))`` into ``arg``. b. Transform ``And(..., And(*args), ...)`` into ``And(..., *args, ...)``. The same for ``Or`` instead of ``And``. 3. Equal arguments: a. Transform ``And(..., arg, ..., arg, ...)`` into ``And(..., arg, ...)``. The same for ``Or`` instead of ``And``. b. Evaluate ``Implies(arg, arg)`` to ``T``. The same for ``Equivalent`` instead of ``Implies``. 4. Sort ``arg_1, ..., arg_n`` within ``And(arg_1, ..., arg_n)`` using a canonical order. The same for ``Or`` instead of ``And``. Overloading of :class:`AtomicFormula <.firstorder.atomic.AtomicFormula>` provides a hook for theories to extend :meth:`simplify` to atomic formulas. .. seealso:: `simplify` methods of classes derived from :class:`AtomicFormula <.firstorder.atomic.AtomicFormula>` within various theories: * :meth:`RCF.atomic.AtomicFormula.simplify <logic1.theories.RCF.atomic.AtomicFormula.simplify>` \ -- real closed fields * :meth:`Sets.atomic.AtomicFormula.simplify <logic1.theories.Sets.atomic.AtomicFormula.simplify>` \ -- theory of Sets More powerful simplifiers provided by various theories: * :func:`RCF.simplify.simplify() \ <logic1.theories.RCF.simplify.simplify>` -- real closed fields, standard simplifier based on implicit theories * :func:`Sets.simplify.simplify() \ <logic1.theories.Sets.simplify.simplify>` -- sets, standard simplifier based on implicit theories """ match self: case _F() | _T(): return self case Not(): arg_simplify = self.arg.simplify() if arg_simplify is _T(): return _F() if arg_simplify is _F(): return _T() return involutive_not(arg_simplify) case And() | Or(): simplified_args: list[Formula] = [] for arg in self.args: arg_simplify = arg.simplify() if arg_simplify is self.definite_element(): return self.definite_element() if arg_simplify is self.neutral_element(): continue if arg_simplify in simplified_args: continue if arg_simplify.op is self.op: simplified_args.extend(arg_simplify.args) else: simplified_args.append(arg_simplify) return self.op(*simplified_args) case Implies(): if self.rhs is _T(): return self.lhs lhs_simplify = self.lhs.simplify() if lhs_simplify is _F(): return _T() rhs_simplify = self.rhs.simplify() if rhs_simplify is _T(): return _T() if lhs_simplify is _T(): return rhs_simplify if rhs_simplify is _F(): return involutive_not(lhs_simplify) assert {lhs_simplify, rhs_simplify}.isdisjoint({_T(), _F()}) if lhs_simplify == rhs_simplify: return _T() return Implies(lhs_simplify, rhs_simplify) case Equivalent(): lhs_simplify = self.lhs.simplify() rhs_simplify = self.rhs.simplify() if lhs_simplify is _T(): return rhs_simplify if rhs_simplify is _T(): return lhs_simplify if lhs_simplify is _F(): if isinstance(rhs_simplify, Not): return rhs_simplify.arg return Not(rhs_simplify) if rhs_simplify is _F(): if isinstance(lhs_simplify, Not): return lhs_simplify.arg return Not(lhs_simplify) if lhs_simplify == rhs_simplify: return _T() return Equivalent(lhs_simplify, rhs_simplify) case All() | Ex(): return self.op(self.var, self.arg.simplify()) case _: # Atomic formulas are caught by the implementation of the # abstract method AtomicFormula.simplify. assert False, type(self)
[docs] def subs(self, substitution: dict[χ, τ | σ]) -> Self: """Substitution of terms for variables. >>> from logic1.theories.RCF import * >>> a, b, x = VV.get('a', 'b', 'x') >>> f = Ex(x, x == a) >>> f.subs({x: a}) Ex(x, a - x == 0) >>> f.subs({a: x}) Ex(G0001_x, -G0001_x + x == 0) >>> g = Ex(x, _ & (b == 0)) >>> g.subs({b: x}) Ex(G0002_x, And(Ex(G0001_x, -G0001_x + G0002_x == 0), x == 0)) """ if Formula.is_quantified_formula(self): # A copy of the mutable could be avoided by keeping track of # the changes and undoing them at the end. substitution = substitution.copy() # (1) Remove substitution for the quantified variable. In # principle, this is covered by (2) below, but deleting here # preserves the name. if self.var in substitution: del substitution[self.var] # Collect all variables on the right hand sides of # substitutions: substituted_vars: set[Variable] = set() for term in substitution.values(): if self.is_term(term): substituted_vars.update(tuple(term.vars())) # (2) Make sure the quantified variable is not a key and does # not occur in a value of substitution: if self.var in substituted_vars or self.var in substitution: var = self.var.fresh() # We now know the following: # (i) var is not a key, # (ii) var does not occur in the values, # (iii) self.var is not a key. # We do *not* know whether self.var occurs in the values. substitution[self.var] = var # All free occurrences of self.var in self.arg will be # renamed to var. In case of (iv) above, substitution will # introduce new free occurrences of self.var, which do not # clash with the new quantified variable var: return self.op(var, self.arg.subs(substitution)) # type: ignore[return-value] return self.op(self.var, self.arg.subs(substitution)) # type: ignore[return-value] elif Formula.is_boolean_formula(self): return_value = self.op(*(arg.subs(substitution) for arg in self.args)) return return_value # type: ignore[return-value] else: # Atomic formulas are caught by the implementation of the # abstract method AtomicFormula.subs. assert False, type(self)
[docs] def to_nnf(self, to_positive: bool = True, _not: bool = False) -> Formula[α, τ, χ, σ]: """Convert to Negation Normal Form. A Negation Normal Form (NNF) is an equivalent formula within which the application of :class:`Not` is restricted to atomic formulas, i.e., instances of :class:`AtomicFormula`, and truth values :data:`T` and :data:`F`. The only other operators admitted are :class:`And`, :class:`Or`, :class:`Ex`, and :class:`All`. If the input is quanitfier-free, :meth:`to_nnf` will not introduce any quanitfiers. If `to_positive` is `True`, :class:`Not` is eliminated via replacing relation symbols with their complements. The result is then even a Positive Normal Form. >>> from logic1.theories.RCF import * >>> a, y = VV.get('a', 'y') >>> f = Equivalent(And(a == 0, T), Ex(y, Not(y == a))) >>> f.to_nnf() And(Or(a != 0, F, Ex(y, a - y != 0)), Or(All(y, a - y == 0), And(a == 0, T))) """ match self: case All() | Ex(): nnf_op: type[Formula[α, τ, χ, σ]] = self.dual() if _not else self.op nnf_arg = self.arg.to_nnf(to_positive=to_positive, _not=_not) return nnf_op(self.var, nnf_arg) case Equivalent(): rewrite: Formula[α, τ, χ, σ] = And(Implies(*self.args), Implies(self.rhs, self.lhs)) return rewrite.to_nnf(to_positive=to_positive, _not=_not) case Implies(): if isinstance(self.rhs, Or): rewrite = Or(Not(self.lhs), *self.rhs.args) else: rewrite = Or(Not(self.lhs), self.rhs) return rewrite.to_nnf(to_positive=to_positive, _not=_not) case And() | Or(): nnf_op = self.dual() if _not else self.op nnf_args: list[Formula] = [] for arg in self.args: nnf_arg = arg.to_nnf(to_positive=to_positive, _not=_not) if nnf_arg.op is nnf_op: nnf_args.extend(nnf_arg.args) else: nnf_args.append(nnf_arg) return nnf_op(*nnf_args) case Not(): return self.arg.to_nnf(to_positive=to_positive, _not=not _not) case _F() | _T(): if _not: return self.dual()() if to_positive else Not(self) return self case AtomicFormula(): if _not: if to_positive: return self.to_complement() return Not(self) return self case _: assert False, type(self)
[docs] def to_pnf(self, prefer_universal: bool = False, is_nnf: bool = False) -> Formula[α, τ, χ, σ]: """Convert to Prenex Normal Form. A Prenex Normal Form (PNF) is a Negation Normal Form (NNF) in which all quantifiers :class:`Ex` and :class:`All` stand at the beginning of the formula. The method used here minimizes the number of quantifier alternations in the prenex block [Burhenne-1990]_. If the minimal number of alternations in the result can be achieved with both :class:`Ex` and :class:`All` as the first quantifier in the result, then the former is preferred. This preference can be changed with a keyword argument `prefer_universal=True`. An keyword argument `is_nnf=True` indicates that `self` is already in NNF. :meth:`to_pnf` then skips the initial NNF computation, which can be useful in time-critical situations. >>> from logic1.theories.RCF import * >>> a, b, y = VV.get('a', 'b', 'y') >>> f = Equivalent(And(a == 0, b == 0, y == 0), ... Ex(y, Or(y == a, a == 0))) >>> f.to_pnf() Ex(G0001_y, All(G0002_y, And(Or(a != 0, b != 0, y != 0, -G0001_y + a == 0, a == 0), Or(And(-G0002_y + a != 0, a != 0), And(a == 0, b == 0, y == 0))))) """ from .pnf import PrenexNormalForm prenex_normal_form: PrenexNormalForm[α, τ, χ, σ] = PrenexNormalForm() return prenex_normal_form(self, prefer_universal, is_nnf)
[docs] def transform_atoms(self, tr: Callable[..., Formula[α, τ, χ, σ]]) -> Formula[α, τ, χ, σ]: """Apply `tr` to all atomic formulas. Replaces each atomic subformula of `self` with the :class:`Formula` `tr(self)`. >>> from logic1.theories.RCF import * >>> x, y, z = VV.get('x', 'y', 'z') >>> f = And(x == y, y < z) >>> f.transform_atoms(lambda atom: atom.op(atom.lhs - atom.rhs, 0)) And(x - y == 0, y - z < 0) """ # Getting rid of the "..." argument of Callable requires ParamSpecs. # Note: Already, before we switched to Generics, there were MyPy # problems with AtomicFormula in that position. match self: case All() | Ex(): return self.op(self.var, self.arg.transform_atoms(tr)) case And() | Or() | Not() | Implies() | Equivalent() | _F() | _T(): args = (arg.transform_atoms(tr) for arg in self.args) return self.op(*args) case AtomicFormula(): return tr(self) case _: # Atomic formulas are caught by the final method # AtomicFormula.transform_atoms. assert False, type(self)
# The following imports are intentionally late to avoid circularity. from .atomic import AtomicFormula, Term, Variable from .boolean import And, BooleanFormula, Equivalent, Implies, involutive_not, Not, Or, _F, _T from .boolean import T # noqa, used in doctests only from .quantified import All, Ex, Prefix, QuantifiedFormula