Complex

Variables, Terms, Atoms

Terms and Variables

Terms and variables in the theory Complex.

Note

The global variable set VV is used to obtain Variables. These can then be recursively combined with Number types using arithmetic +, -, *, /, **, the imaginary unit I, and the functions Re, Im, and Conj to build larger Terms. The symbol ~ is an alias for Conj.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> Re(z + I)
1/2 * z + 1/2 * ~z

logic1.theories.Complex.term.VV: Final[VariableSet] = {...}

The global VariableSet used in the theory of complex numbers.

>>> VV['z']
z
>>> VV.get('a', 'b')
(a, b)

logic1.theories.Complex.term.Re(term: Term) → Term

Return the real part of a term.

>>> Re(2 * I)
0
>>> z = VV['z']
>>> Re(z)
1/2 * z + 1/2 * ~z

logic1.theories.Complex.term.Im(term: Term) → Term

Return the imaginary part of a term.

>>> Im(2 * I)
2
>>> z = VV['z']
>>> Im(z)
-1/2 * I * z + 1/2 * I * ~z

logic1.theories.Complex.term.Conj(term: Term) → Term

Return the complex conjugate of a term.

>>> z = VV['z']
>>> Conj(z + 2)
~z + 2
>>> Conj(2 * I)
-2 * I

logic1.theories.Complex.term.I: Final[Term] = I

The imaginary unit.

>>> I**2
-1

class logic1.theories.Complex.term.Term

Bases: Term[Term, Variable, int | float | Fraction | mpq | complex, SortKey]

Term in the theory of complex numbers. Implements the abstract class firstorder.term.Term. It is represented internally as AST in normal form. The default normal form is conjugate_normal_form(), but it can be changed globally using set_normal_form().

>>> z = VV['z']
>>> (z + I) ** 2
z**2 + 2 * I * z - 1
>>> Re(z)
1/2 * z + 1/2 * ~z

See also

Variable, VV, Re(), Im(), Conj(), AtomicFormula

property normal_ast: AST

The AST representation of this term in the global normal form.

__init__(number: int | float | Fraction | mpq | complex) → None

Initialize a term from a number.

>>> Term(2)
2
>>> Term(1.5)
3/2
>>> Term(1 + 2j)
1 + 2 * I

__add__(other: int | float | Fraction | mpq | complex | Term) → Term

Add another term or a number to this term.

>>> z = VV['z']
>>> z + 2
z + 2

__eq__(other: int | float | Fraction | mpq | complex | Term) → Eq

Construct an equality between this term and another term or a number.

>>> z = VV['z']
>>> z == 2
z == 2

__ge__(other: int | float | Fraction | mpq | complex | Term) → Ge

Construct a non-strict inequality between this term and another term or a number. Raise a ValueError if either side of the inequality is not real.

>>> z = VV['z']
>>> z * ~z >= 0
z * ~z >= 0
>>> z >= 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z >= 0 because it is not real

__gt__(other: int | float | Fraction | mpq | complex | Term) → Gt

Construct a strict inequality between this term and another term or a number. Raise a ValueError if either side of the inequality is not real.

>>> z = VV['z']
>>> z * ~z > 0
z * ~z > 0
>>> z > 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z > 0 because it is not real

__invert__() → Term

Return the complex conjugate of this term.

>>> ~I
-I

__le__(other: int | float | Fraction | mpq | complex | Term) → Le

Construct a non-strict inequality between this term and another term or a number. Raise a ValueError if either side of the inequality is not real.

>>> z = VV['z']
>>> z * ~z <= 0
z * ~z <= 0
>>> z <= 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z <= 0 because it is not real

__lt__(other: int | float | Fraction | mpq | complex | Term) → Lt

Construct a strict inequality between this term and another term or a number. Raise a ValueError if either side of the inequality is not real.

>>> z = VV['z']
>>> z * ~z < 0
z * ~z < 0
>>> z < 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z < 0 because it is not real

__mul__(other: int | float | Fraction | mpq | complex | Term) → Term

Multiply this term by another term or a number.

>>> z = VV['z']
>>> z * 2
2 * z

__ne__(other: int | float | Fraction | mpq | complex | Term) → Ne

Construct an inequality between this term and another term or a number.

>>> z = VV['z']
>>> z != 2
z != 2

__neg__() → Term

Return the negation of this term.

>>> z = VV['z']
>>> -z
-z

__pow__(other: int) → Term

Raise this term to a non-negative integer power. Raise a ValueError if the exponent is negative.

>>> I ** 2
-1

__repr__() → str

Return a string representation of this term that is valid Python code and allows for the reconstruction of the original term.

>>> z = VV['z']
>>> repr(z ** 2 + I)
'z**2 + I'

__str__() → str

Return a human-readable string representation of this term.

>>> z = VV['z']
>>> str(z ** 2 + I)
'z^2 + i'

__sub__(other: int | float | Fraction | mpq | complex | Term) → Term

Subtract another term or a number from this term.

>>> z = VV['z']
>>> z - 2
z - 2

__truediv__(other: int | float | Fraction | mpq | complex | Term) → Term

Divide this term by another term or a number. Raise a ValueError if the other term is not constant.

>>> z = VV['z']
>>> z / 2
1/2 * z
>>> z / z
Traceback (most recent call last):
...
ValueError: Cannot divide by a non-constant term

__xor__(other: Never) → Term

Raise a NotImplementedError. The operator ** is used for exponentiation instead.

as_latex() → str

Return a LaTeX representation as a string. Implements the abstract method firstorder.term.Term.as_latex().

>>> z = VV['z']
>>> (z + 2 * I).as_latex()
'z + 2 i'

as_variable() → Variable

Return this term as a variable. Raises a ValueError if this term is not a variable.

>>> z = VV['z']
>>> z.as_variable()
z
>>> (z + 1).as_variable()
Traceback (most recent call last):
...
ValueError: Term z + 1 is not a variable

conjugate() → Term

Return the complex conjugate of this term.’

>>> z = VV['z']
>>> (z + 2).conjugate()
~z + 2
>>> (2 * I).conjugate()
-2 * I

See also

Conj(), ~

eval() → tuple[mpq, mpq]

Evaluate this term to a pair of its real and imaginary parts. Raise a ValueError if this term is not constant.

>>> (1 + 2 * I).eval()
(mpq(1,1), mpq(2,1))
>>> z = VV['z']
>>> (z + 2).eval()
Traceback (most recent call last):
...
ValueError: Cannot evaluate variable z

static from_real_imag(real: int | float | Fraction | mpq, imag: int | float | Fraction | mpq) → Term

Convert a pair of real and imaginary parts to a term.

>>> Term.from_real_imag(1, 2)
1 + 2 * I

imaginary_part() → Term

Return the imaginary part of this term.

>>> (2 * I).imaginary_part()
2
>>> z = VV['z']
>>> (z + 2).imaginary_part()
-1/2 * I * z + 1/2 * I * ~z

See also

Im()

is_constant() → bool

Return True if this term is constant.

>>> x = VV['x']
>>> (x + 2).is_constant()
False
>>> (2 * I).is_constant()
True

is_imaginary() → bool

Return True if this term is imaginary, i.e., its real part is zero.

>>> x = VV['x']
>>> (x + 2).is_imaginary()
False
>>> (2 * I).is_imaginary()
True

is_real() → bool

Return True if this term is real, i.e., its imaginary part is zero.

>>> x = VV['x']
>>> (x + 2).is_real()
False
>>> (x + x.conjugate()).is_real()
True

is_variable() → bool

Return True if this term is a variable.

>>> x = VV['x']
>>> (x + 2).is_variable()
False
>>> x.is_variable()
True
>>> I.is_variable()
False

is_zero() → bool

Return True if this term is zero.

>>> x = VV['x']
>>> (x + 2).is_zero()
False
>>> (x - x).is_zero()
True

lc() → Term

Return the leading coefficient of this term.

>>> z = VV['z']
>>> (3 * z - 2).lc()
3
>>> (-z * ~z).lc()
-1

real_part() → Term

Return the real part of this term.

>>> (2 * I).real_part()
0
>>> z = VV['z']
>>> z.real_part()
1/2 * z + 1/2 * ~z

See also

Re()

classmethod set_normal_form(normalizer: Callable[[AST], AST]) → Callable[[AST], AST]

Set the global normal form for terms and return the previous used normal form. The default normal form is conjugate_normal_form().

>>> z = VV['z']
>>> z
z
>>> old = Term.set_normal_form(cartesian_normal_form)
>>> z
Re(z) + I * Im(z)
>>> old == conjugate_normal_form
True
>>> _ = Term.set_normal_form(old)
>>> z
z

See also

conjugate_normal_form(), cartesian_normal_form()

sort_key() → SortKey[Self]

Return a sort key suitable for ordering terms. Implements the abstract method firstorder.term.Term.sort_key().

>>> z = VV['z']
>>> z.sort_key() < (z + 1).sort_key()
True

subs(sigma: Mapping[Variable, int | float | Fraction | mpq | complex | Term]) → Term

Return a term obtained by substituting the variables in this term according to the given mapping.

>>> a, b = VV.get('a', 'b')
>>> (a ** 2).subs({a: I})
-1
>>> (a + b).subs({a: 1, b: a})
a + 1

vars() → Iterator[Variable]

Return an iterator that yields each variable of this term once. Implements the abstract method firstorder.term.Term.vars().

>>> a, b, c = VV.get('a', 'b', 'c')
>>> vars = (a + b * c).vars()
>>> list(sorted(vars, key=Term.sort_key))
[a, b, c]

class logic1.theories.Complex.term.SortKey

Bases: Generic[τ]

A sort key for terms.

>>> z = VV['z']
>>> SortKey(z) < SortKey(z + 1)
True

See also

Term.sort_key()

term: τ

The Term for which this is a sort key.

__le__(other: SortKey) → bool

Comparison of terms based on ast.SortKey. The remaining comparison operators are derived from this using functools.total_ordering().

>>> z = VV['z']
>>> SortKey(z) <= SortKey(z)
True
>>> SortKey(z) <= SortKey(z + 1)
True

class logic1.theories.Complex.term.Variable

Bases: Term, Variable[Variable, int | float | Fraction | mpq | complex, SortKey[Variable]]

Variable in the theory of complex numbers. Implements the abstract class firstorder.term.Variable. Variables are obtained from the global variable set VV.

>>> VV['z']
z
>>> VV.get('a', 'b')
(a, b)

property name: str

The name of this variable.

>>> z = VV['z']
>>> z.name
'z'

__init__() → None

This constructor is not meant to be called directly. Use VV to create variables.

fresh() → Variable

Return a variable that has not been used so far. Implements abstract method firstorder.term.Variable.fresh().

>>> z = VV['z']
>>> z.fresh()
G0001_z

class logic1.theories.Complex.term.VariableSet

Bases: VariableSet[Variable]

Infinite set of variables used in the theory of complex numbers. Implements the abstract class firstorder.term.VariableSet. Variables are obtained from the global instance VV.

>>> VV['z']
z
>>> VV.get('a', 'b')
(a, b)

property stack: list[set[str]]

Return the current stack of variable names. Implements the abstract property firstorder.term.VariableSet.stack.

>>> VV.reset()
>>> z = VV['z']
>>> VV.stack
[{'z'}]

__getitem__(index: str) → Variable

Return the variable with the given name. Implements the abstract method firstorder.term.VariableSet.__getitem__().

>>> VV['z']
z

__repr__() → str

Return a string representation of this variable set.

>>> VV.reset()
>>> VV.get('x', 'y', 'z')
(x, y, z)
>>> VV
{x, y, z, ...}

fresh(suffix: str = '') → Variable

Return a fresh variable, by default from the sequence G0001, G0002, …, G9999, G10000, … This naming convention is inspired by Lisp’s gensym(). If the optional argument suffix is specified, the sequence G0001<suffix>, G0002<suffix>, … is used instead.

>>> VV.fresh()
G0001

pop() → None

Raise a NotImplementedError. Implements the abstract method firstorder.term.VariableSet.pop().

push() → None

Raise a NotImplementedError. Implements the abstract method firstorder.term.VariableSet.push().

reset() → None

Clear all used variable names.

>>> VV.reset()
>>> z = VV['z']
>>> VV
{z, ...}
>>> VV.reset()
>>> VV
{...}

__eq__(other)

Return self==value.

__init__(_names: set[str] = <factory>) → None

Atomic Formulas

Atomic formulas in the theory Complex.

Note

Atomic formulas can be constructed from terms using the standard comparison operators (==, !=, <, <=, >, >=). Note that inequalities can only be constructed if both sides are real, otherwise a ValueError is raised.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> z == 1
z == 1
>>> Re(z) >= 0
1/2 * z + 1/2 * ~z >= 0
>>> z > 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z > 0 because it is not real

class logic1.theories.Complex.atomic.AtomicFormula

Bases: AtomicFormula[AtomicFormula, Term, Variable, int | float | Fraction | mpq | complex]

Abstract base class for atomic formulas in the theory of complex numbers. Implements the abstract class firstorder.atomic.AtomicFormula.

See also

Eq, Ne, Ge, Gt, Le, Lt

property lhs: Term

The left-hand side term of this atomic formula.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> (z == 0).lhs
z

property rhs: Term

The right-hand side term of this atomic formula.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> (z == 0).rhs
0

__bool__() → bool

Compare the sort keys of both sides of this atomic formula using the corresponding operator of this formula. This is used to evaluate atomic formulas in Boolean contexts. For evaluating constant atomic formulas with respect to their usual semantics, use eval() instead.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> bool(z == 0)
False
>>> bool(z != 0)
True
>>> bool(z * ~z >= 1)  # not the usual semantics!
True

__le__(other: Formula) → bool

Compare this atomic formula with another formula. Implements the abstract method firstorder.atomic.AtomicFormula.__le__().

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> (z == 0) <= (z != 0)
True

__repr__() → str

Return a string representation of this atomic formula that is valid Python code and can be evaluated to reconstruct the original atomic formula.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> repr(z == 0)
'z == 0'

__str__() → str

Return a string representation of this atomic formula. Implements the abstract method firstorder.atomic.AtomicFormula.__str__().

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> str(z == 0)
'z = 0'

as_latex() → str

Return a LaTeX representation of this atomic formula. Implements the abstract method firstorder.atomic.AtomicFormula.as_latex().

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> (z * ~z >= 0).as_latex()
'z \\overline{z} \\geq 0'

bvars(quantified: frozenset[Variable] = frozenset({})) → Iterator[Variable]

Return an iterator over occurrences of variables that are elements of quantified. Yield each such variable once for each term that it occurs in. Implements the abstract method firstorder.atomic.AtomicFormula.bvars().

classmethod complement() → type[AtomicFormula]

Return the complement relation. Implements the abstract method firstorder.atomic.AtomicFormula.complement().

See also

Inherited method firstorder.atomic.AtomicFormula.to_complement()

>>> Eq.complement()
<class 'logic1.theories.Complex.atomic.Ne'>
>>> Lt.complement()
<class 'logic1.theories.Complex.atomic.Ge'>

classmethod converse() → type[AtomicFormula]

Return the converse relation.

>>> Le.converse()
<class 'logic1.theories.Complex.atomic.Ge'>
>>> Lt.converse()
<class 'logic1.theories.Complex.atomic.Gt'>

eval() → bool

Evaluate an atomic formula where both sides are constants. Return True if the formula equivalent to T. Raises ValueError if the formula contains variables.

>>> from logic1.theories.Complex import *
>>> (2 * I == 0).eval()
False
>>> (I**2 < 0).eval()
True
>>> x = VV['x']
>>> (x == 0).eval()
Traceback (most recent call last):
...
ValueError: Cannot evaluate variable x

fvars(quantified: frozenset[Variable] = frozenset({})) → Iterator[Variable]

Return an iterator over occurrences of variables that are not elements of quantified. Yield each such variable once for each term that it occurs in. Implements the abstract method firstorder.atomic.AtomicFormula.fvars().

is_imaginary() → bool

Return True if both sides of this atomic formula are imaginary.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> (Re(z) == 0).is_imaginary()
False
>>> (I * Re(z) == 0).is_imaginary()
True

is_real() → bool

Return True if both sides of this atomic formula are real.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> (z == 0).is_real()
False
>>> (z * ~z == 0).is_real()
True

real_normal_form() → Formula

Return an equivalent formula in real normal form.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> (z == 0).real_normal_form()
And(1/2 * z + 1/2 * ~z == 0, -1/2 * I * z + 1/2 * I * ~z == 0)
>>> (z != 0).real_normal_form()
Or(1/2 * z + 1/2 * ~z != 0, -1/2 * I * z + 1/2 * I * ~z != 0)

simplify() → AtomicFormula | _T | _F

Return an equivalent simplified version of this atomic formula. Implements the abstract method firstorder.atomic.AtomicFormula.simplify().

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> (z * ~z == Re(z)**2 + Im(z)**2).simplify()
T
>>> (Re(z) == 0).simplify()
z + ~z == 0
>>> (-Re(z) > z * ~z).simplify()
z * ~z + 1/2 * z + 1/2 * ~z < 0

subs(sigma: Mapping[Variable, int | float | Fraction | mpq | complex | Term]) → Self

Formal simultaneous term substitution into both sides of the atomic formula. Implements the abstract method firstorder.atomic.AtomicFormula.subs().

>>> from logic1.theories.Complex import *
>>> a, b = VV.get('a', 'b')
>>> (a + b == 0).subs({a: 1, b: a})
a + 1 == 0

class logic1.theories.Complex.atomic.RealAtomicFormula

Bases: AtomicFormula

An abstract base class for atomic formulas where both sides are real. Raise a ValueError when trying to create an instance where either side is not real.

See also

Ge, Le, Gt, Lt

abstractmethod __init__(lhs: int | float | Fraction | mpq | complex | Term, rhs: int | float | Fraction | mpq | complex | Term)

Initialize the real atomic formula. Raise a ValueError if either side is not real. This abstract base class is not supposed to have instances itself.

class logic1.theories.Complex.atomic.Eq

Bases: AtomicFormula

Equality relation in the theory of complex numbers.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> z == 0
z == 0

__init__(lhs: int | float | Fraction | mpq | complex | Term, rhs: int | float | Fraction | mpq | complex | Term) → None

Initialize the equality relation.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> Eq(z, 0)
z == 0

class logic1.theories.Complex.atomic.Ne

Bases: AtomicFormula

Inequality relation in the theory of complex numbers.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> z != 0
z != 0

__init__(lhs: int | float | Fraction | mpq | complex | Term, rhs: int | float | Fraction | mpq | complex | Term) → None

Initialize the inequality relation.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> Ne(z, 0)
z != 0

class logic1.theories.Complex.atomic.Le

Bases: RealAtomicFormula

Less than or equal relation in the theory of complex numbers.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> z * ~z <= 0
z * ~z <= 0
>>> z <= 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z <= 0 because it is not real

__init__(lhs: int | float | Fraction | mpq | complex | Term, rhs: int | float | Fraction | mpq | complex | Term) → None

Initialize the less than or equal relation.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> Le(z * ~z, 0)
z * ~z <= 0
>>> Le(z, 0)
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z <= 0 because it is not real

class logic1.theories.Complex.atomic.Ge

Bases: RealAtomicFormula

Greater than or equal relation in the theory of complex numbers.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> z * ~z >= 0
z * ~z >= 0
>>> z >= 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z >= 0 because it is not real

__init__(lhs: int | float | Fraction | mpq | complex | Term, rhs: int | float | Fraction | mpq | complex | Term) → None

Initialize the greater than or equal relation. Raise a ValueError if either side is not real.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> Ge(z * ~z, 0)
z * ~z >= 0
>>> Ge(z, 0)
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z >= 0 because it is not real

class logic1.theories.Complex.atomic.Lt

Bases: RealAtomicFormula

Less than relation in the theory of complex numbers.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> z * ~z < 0
z * ~z < 0
>>> z < 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z < 0 because it is not real

__init__(lhs: int | float | Fraction | mpq | complex | Term, rhs: int | float | Fraction | mpq | complex | Term) → None

Initialize the less than relation. Raise a ValueError if either side is not real.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> Lt(z * ~z, 0)
z * ~z < 0
>>> Lt(z, 0)
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z < 0 because it is not real

class logic1.theories.Complex.atomic.Gt

Bases: RealAtomicFormula

Greater than relation in the theory of complex numbers.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> z * ~z > 0
z * ~z > 0
>>> z > 0
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z > 0 because it is not real

__init__(lhs: int | float | Fraction | mpq | complex | Term, rhs: int | float | Fraction | mpq | complex | Term) → None

Initialize the greater than relation.

>>> from logic1.theories.Complex import *
>>> z = VV['z']
>>> Gt(z * ~z, 0)
z * ~z > 0
>>> Gt(z, 0)
Traceback (most recent call last):
...
ValueError: Cannot create atomic formula z > 0 because it is not real