"""We introduce formulas with Boolean toplevel operators as subclasses of
:class:`.Formula`.
"""
from __future__ import annotations
from typing import final, Optional
from .atomic import AtomicFormula, Term, Variable
from .formula import α, τ, χ, σ, Formula
from ..support.tracing import trace # noqa
[docs]
@final
class Equivalent(BooleanFormula[α, τ, χ, σ]):
r"""A class whose instances are equivalences in the sense that their
toplevel operator represents the Boolean operator
:math:`\longleftrightarrow`.
>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> Equivalent(x >= 0, Or(x > 0, x == 0))
Equivalent(x >= 0, Or(x > 0, x == 0))
"""
@property
def lhs(self) -> Formula[α, τ, χ, σ]:
"""The left-hand side of the equivalence.
.. seealso::
* :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
* :attr:`op <.formula.Formula.op>` -- operator
"""
return self.args[0]
@property
def rhs(self) -> Formula[α, τ, χ, σ]:
"""The right-hand side of the equivalence.
.. seealso::
* :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
* :attr:`op <.formula.Formula.op>` -- operator
"""
return self.args[1]
def __init__(self, lhs: Formula[α, τ, χ, σ], rhs: Formula[α, τ, χ, σ]) -> None:
self.args = (lhs, rhs)
[docs]
@final
class Implies(BooleanFormula[α, τ, χ, σ]):
"""A class whose instances are equivalences in the sense that their
toplevel operator represents the Boolean operator :math:`\\longrightarrow`.
>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> Implies(x == 0, x >= 0)
Implies(x == 0, x >= 0)
.. seealso::
* :meth:`>>, __rshift__() <.formula.Formula.__rshift__>` -- \
infix notation of :class:`Implies`
* :meth:`\\<\\<, __lshift__() <.formula.Formula.__lshift__>` -- \
infix notation of converse :class:`Implies`
""" # noqa
@property
def lhs(self) -> Formula[α, τ, χ, σ]:
"""The left-hand side of the implication.
.. seealso::
* :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
* :attr:`op <.formula.Formula.op>` -- operator
"""
return self.args[0]
@property
def rhs(self) -> Formula[α, τ, χ, σ]:
"""The right-hand side of the implication.
.. seealso::
* :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
* :attr:`op <.formula.Formula.op>` -- operator
"""
return self.args[1]
def __init__(self, lhs: Formula[α, τ, χ, σ], rhs: Formula[α, τ, χ, σ]) -> None:
self.args = (lhs, rhs)
[docs]
@final
class And(BooleanFormula[α, τ, χ, σ]):
"""A class whose instances are conjunctions in the sense that their
toplevel operator represents the Boolean operator
:math:`\\wedge`.
>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> And()
T
>>> And(x == 0)
x == 0
>>> And(x == 1, x == y, y == z)
And(x - 1 == 0, x - y == 0, y - z == 0)
.. seealso::
* :meth:`&, __and__() <.formula.Formula.__and__>` -- \
infix notation of :class:`And`
* :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
* :attr:`op <.formula.Formula.op>` -- operator
"""
[docs]
@classmethod
def dual(cls) -> type[Or[α, τ, χ, σ]]:
r"""A class method yielding the class :class:`Or`, which implements
the dual operator :math:`\vee` of :math:`\wedge`.
"""
return Or
[docs]
@classmethod
def definite(cls) -> type[_F[α, τ, χ, σ]]:
r"""A class method yielding the class :class:`_F`, which is the
operator of the constant Formula :data:`F`. The definite is the dual of
the neutral.
"""
return _F
[docs]
@classmethod
def definite_element(cls) -> _F[α, τ, χ, σ]:
r"""A class method yielding the unique instance :data:`F` of the
:class:`_F`.
"""
return _F()
[docs]
@classmethod
def neutral(cls) -> type[_T[α, τ, χ, σ]]:
r"""A class method yielding the class :class:`_T`, which is the
operator of the constant Formula :data:`T`. The neutral is the dual of
the definite.
"""
return _T
[docs]
@classmethod
def neutral_element(cls) -> _T[α, τ, χ, σ]:
r"""A class method yielding the unique instance :data:`T` of the
:class:`_T`.
"""
return _T()
def __new__(cls, *args: Formula[α, τ, χ, σ]):
if not args:
return T
if len(args) == 1:
return args[0]
return super().__new__(cls)
def __init__(self, *args: Formula[α, τ, χ, σ]) -> None:
"""
>>> from logic1.theories.RCF import *
>>> a, = VV.get('a')
>>> And(a >= 0, a != 0)
And(a >= 0, a != 0)
"""
args_flat = []
for arg in args:
if isinstance(arg, And):
args_flat.extend(list(arg.args))
else:
args_flat.append(arg)
self.args = tuple(args_flat)
[docs]
@final
class Or(BooleanFormula[α, τ, χ, σ]):
"""A class whose instances are disjunctions in the sense that their
toplevel operator represents the Boolean operator
:math:`\\vee`.
>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> Or()
F
>>> Or(x == 0)
x == 0
>>> Or(x == 1, x == 2, x == 3)
Or(x - 1 == 0, x - 2 == 0, x - 3 == 0)
.. seealso::
* :meth:`|, __or__() <.formula.Formula.__or__>` -- \
infix notation of :class:`Or`
* :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
* :attr:`op <.formula.Formula.op>` -- operator
"""
[docs]
@classmethod
def dual(cls) -> type[And[α, τ, χ, σ]]:
r"""A class method yielding the class :class:`And`, which implements
the dual operator :math:`\wedge` of :math:`\vee`.
"""
return And
[docs]
@classmethod
def definite(cls) -> type[_T[α, τ, χ, σ]]:
r"""A class method yielding the class :class:`_T`, which is the
operator of the constant Formula :data:`T`. The definite is the dual of
the neutral.
"""
return _T
[docs]
@classmethod
def definite_element(cls) -> _T[α, τ, χ, σ]:
r"""A class method yielding the unique instance :data:`T` of the
:class:`_T`.
"""
return _T()
[docs]
@classmethod
def neutral(cls) -> type[_F[α, τ, χ, σ]]:
r"""A class method yielding the class :class:`_F`, which is the
operator of the constant Formula :data:`F`. The neutral is the dual of
the definite.
"""
return _F
[docs]
@classmethod
def neutral_element(cls) -> _F[α, τ, χ, σ]:
r"""A class method yielding the unique instance :data:`F` of the
:class:`_F`.
"""
return _F()
def __new__(cls, *args: Formula[α, τ, χ, σ]):
if not args:
return F
if len(args) == 1:
return args[0]
return super().__new__(cls)
def __init__(self, *args: Formula[α, τ, χ, σ]) -> None:
"""
>>> from logic1.theories.RCF import *
>>> a, = VV.get('a')
>>> Or(a > 0, a == 0)
Or(a > 0, a == 0)
"""
args_flat = []
for arg in args:
if isinstance(arg, Or):
args_flat.extend(list(arg.args))
else:
args_flat.append(arg)
self.args = tuple(args_flat)
[docs]
@final
class Not(BooleanFormula[α, τ, χ, σ]):
"""A class whose instances are negated formulas in the sense that their
toplevel operator is the Boolean operator
:math:`\\neg`.
>>> from logic1.theories.RCF import *
>>> a, = VV.get('a')
>>> Not(a == 0)
Not(a == 0)
.. seealso::
* :meth:`~, __invert__() <.formula.Formula.__invert__>` -- \
short notation of :class:`Not`
"""
@property
def arg(self) -> Formula[α, τ, χ, σ]:
"""The one argument of the operator :math:`\\neg`.
.. seealso::
* :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
* :attr:`op <.formula.Formula.op>` -- operator
"""
return self.args[0]
def __init__(self, arg: Formula[α, τ, χ, σ]) -> None:
"""
>>> from logic1.theories.RCF import *
>>> a, = VV.get('a')
>>> Not(a == 0)
Not(a == 0)
"""
self.args = (arg, )
[docs]
def involutive_not(arg: Formula[α, τ, χ, σ]) -> Formula[α, τ, χ, σ]:
"""Construct a formula equivalent Not(arg) using the involutive law if
applicable.
>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> involutive_not(x == 0)
Not(x == 0)
>>> involutive_not(Not(x == 0))
x == 0
>>> involutive_not(T)
Not(T)
"""
if isinstance(arg, Not):
return arg.arg
return Not(arg)
[docs]
@final
class _T(BooleanFormula[α, τ, χ, σ]):
"""A singleton class whose sole instance represents the constant Formula
that is always true.
>>> _T()
T
>>> _T() is _T()
True
"""
# This is a quite basic implementation of a singleton class. It does not
# support subclassing. We do not use a module because we need _T to be a
# subclass itself.
[docs]
@classmethod
def dual(cls) -> type[_F[α, τ, χ, σ]]:
r"""A class method yielding the class :class:`_F`, which implements
the dual operator :math:`\bot` of :math:`\top`.
"""
return _F
_instance: Optional[_T[α, τ, χ, σ]] = None
def __init__(self) -> None:
self.args = ()
def __new__(cls):
if cls._instance is None:
cls._instance = super().__new__(cls)
return cls._instance
def __repr__(self) -> str:
return 'T'
T: _T['AtomicFormula', 'Term', 'Variable', object] = _T()
"""Support use as a constant without parentheses.
We instantiate type variables with their respective upper bounds, which is the
best we can do at the module level. `T` cannot be generic. Therefore, _T()
should be used within statically typed code instead.
>>> T is _T()
True
"""
[docs]
@final
class _F(BooleanFormula[α, τ, χ, σ]):
"""A singleton class whose sole instance represents the constant Formula
that is always false.
>>> _F()
F
>>> _F() is _F()
True
"""
# This is a quite basic implementation of a singleton class. It does not
# support subclassing. We do not use a module because we need _F to be a
# subclass itself.
[docs]
@classmethod
def dual(cls) -> type[_T[α, τ, χ, σ]]:
r"""A class method yielding the class :class:`_T`, which implements
the dual operator :math:`\top` of :math:`\bot`.
"""
return _T
_instance: Optional[_F[α, τ, χ, σ]] = None
def __init__(self) -> None:
self.args = ()
def __new__(cls):
if cls._instance is None:
cls._instance = super().__new__(cls)
return cls._instance
def __repr__(self) -> str:
return 'F'
F: _F['AtomicFormula', 'Term', 'Variable', object] = _F()
"""Support use as a constant without parentheses.
We instantiate type variables with their respective upper bounds, which is the
best we can do at the module level. `F` cannot be generic. Therefore, _F()
should be used within statically typed code instead.
>>> F is _F()
True
"""