`pytableaux.lang`

Lexical Base Classes 

Base Lexical class. This is the base class from which all concrete lexical classes inherit, including enum classes. It provides basic features of identitfying, comparing, and generating items.

The ident and spec attributes provide canonical ways of specifying items with tuples of numbers, strings, and other tuples. This is useful for serialization and deserialization.

The first(), next(), and gen() methods enable programatic creation of items.

The hash and sort_tuple attributes allow for rich comparison and ordering of items, with consistency for comparing across different types.

The TYPE refers to the corresponding member of the special LexType enum class member, which holds meta information about each type.

TYPE: ClassVar[LexType]: LexType enum instance for concrete classes.

spec: tuple: The arguments roughly needed to construct, given that we know the type, i.e. in intuitive order. A tuple, possibly nested, containing numbers or strings.

ident: tuple[str, tuple]: Equality identifier able to compare across types. Equivalent to (classname, spec).

sort_tuple: tuple[int, ...]: Sorting identifier, to order tokens of the same type, consisting of non-negative integers. This is also used in hashing, so equal objects must have equal sort_tuple values.

hash: int: The integer hash. Same as hash(obj).

classmethod first()[source]

Get the canonically first item of the type. This can be called on both concrete and abstract classes. For example:

>>> Atomic.first()
<Sentence: A>
>>> Constant.first()
<Parameter: a>
>>> Constant.first() == Parameter.first()
True
>>> Operated.first()
<Sentence: ⚬A>
>>> Lexical.first()
<Predicate: F>
>>> LexicalEnum.first()
<Quantifier: Existential>

Return type:: Self

abstract next(**kw)[source]

Get the canonically next item of the type. Various subclasses may provide optional keyword arguments.

Return type:: Self

classmethod gen(stop, /, first=None, **nextkw)[source]

Generate items of the type, using first() and next() methods.

This is convenient for making sequential lexical items quickly, without going through parsing.

>>> Predicate(1,0,4)(Constant.gen(4))
<Sentence: Gabcd>

Parameters:

stop (int | None) -- The number at which to stop generating. If None, never stop.
first (Self | None) -- The first item. If None, starts with first().

Keyword Arguments:

**nextkw -- Parameters to pass to each call to next().

Returns:

The generator instance.

Return type:

Iterator[Self]

static orderitems(lhs: Lexical, rhs: Lexical, /) → int[source]

Pairwise ordering comparison based on type rank and sort_tuple. This is the base method used to support equality and rich comparison operators between any Lexical instance, regardless of subclass.

Parameters:

lhs (Lexical) -- The left-hand item.
rhs (Lexical) -- The right-hand item.

Returns:

The relative order of lhs and rhs. The return value

will be either:

Less than 0 if lhs precedes rhs in order.

Greater than 0 if rhs precedes lhs in order.

Equal to 0 if lhs is equal to rhs in order.

Return type:

int

Raises:

TypeError -- if an argument is not an instance of Lexical with a valid sort_tuple attribute.

class LexicalEnum[source]

Bases: Lexical, LangCommonEnum

Base class for Enum lexical classes. Subclassed by Quantifier and Operator.

Parameters:: value (object) --
Return type:: _EnumT

index: int: The member index in the members sequence.

order: int: A number to signify relative member order (need not be sequence index).

label: str: Label with spaces allowed.

strings: frozenset[str]: Name, label, or other strings unique to a member.

class CoordsItem[source]

Common implementation for lexical types that are based on integer coordinates. For Constant, Variable, and Atomic, the coordinates are (index, subscript). For Predicate, the coordinates are (index, subscript, arity).

index: int: The index coordinate.

subscript: int: The subscript coordinate.

class Parameter[source]

Bases: CoordsItem

Parameter base class for Constant & Variable.

class Sentence[source]

Bases: LexicalAbc

Sentence base class. This provides common attributes and methods for the concrete sentence classes Atomic, Predicated, Quantified, and Operated.

Behaviors

Sentences support the built-in operators ~, |, and &, for negation, disjunction, and conjunction, respectively.

>>> a, b = Sentence.gen(2)
>>> ~a == a.negate()
True
>>> a | b == a.disjoin(b)
True
>>> a & b == a.conjoin(b)
True

predicates: frozenset[Predicate]: Set of predicates, recursive.

constants: frozenset[Constant]: Set of constants, recursive.

variables: frozenset[Variable]: Set of variables, recursive.

atomics: frozenset[Atomic]: Set of atomic sentences, recursive.

quantifiers: tuple[Quantifier, ...]: Sequence of quantifiers, recursive.

operators: tuple[Operator, ...]: Sequence of operators, recursive.

negate()[source]

Negate this sentence, returning the new sentence. This can also be invoked using the ~ operator.

Returns:: The new sentence.

asserted()[source]

Apply the Assertion operator. This can also be invoked using the + operator.

Returns:: The new sentence.

disjoin(rhs, /)[source]

Apply the Disjunction operator to the right-hand sentence. This can also be invoked using the | operator.

Parameters:: rhs (Sentence) -- The right-hand disjunct.
Returns:: The new sentence.

conjoin(rhs, /)[source]

Apply the Conjunction operator to the right-hand sentence. This can also be invoked using the & operator.

Parameters:: rhs (Sentence) -- The right-hand conjunct.
Returns:: The new sentence.

negative()[source]

Either negate this sentence, or, if this is already a negated sentence return its negatum, i.e., "un-negate" the sentence. This can also be invoked using the - operator.

>>> a = Atomic.first()
>>> a.negate() == a.negative()
True
>>> a.negate().negative() == a
True

Returns:: The new sentence.
Return type:: Sentence

substitute(pnew, pold, /)[source]

Return the recursive substitution of pnew for all occurrences of pold.

Parameters:

pnew (Parameter) -- The new parameter.
pold (Parameter) -- The old parameter.

Returns:

The new sentence.

Return type:

Self

Concrete Lexical Classes 

Predicate 

class Predicate[source]

A predicate is specified by an integer 3-tuple of (index, subscript, arity). The index can range from 0-3, and the subscript and arity can be any positive integer.

To create a predicate, the spec can be passed either as separate arguments, or as a single tuple:

>>> p = Predicate(0, 0, 1)
>>> p == Predicate((0, 0, 1))
True

System Predicates

There are two built-in system predicates, Identity and Existence. These are specified internal by the special indexes -1 and -2, respectively. They are defined in an enum class Predicate.System, and can be accessed in several ways:

>>> p = Predicate('Identity')
>>> p is Predicate.Identity
True
>>> p is Predicate.System.Identity
True

System predicates are considered equal to their name.

>>> Predicate.Identity == 'Identity'
True

Behaviors

Calling a predicate will construct a Predicated sentence:

>>> p = Predicate(0, 0, 2)
>>> a, b = Constant.gen(2)
>>> p((a, b)) == Predicated(p, (a, b))
True

property is_system: bool: Whether this is a system predicate.

bicoords: BiCoords: The symbol coordinates (index, subscript).

arity: int: The predicate's arity.

name: tuple[int, ...] | str

The name, for system predicates. For non-system predicates, this is the same as the spec.

>>> Predicate.Identity.name
'Identity'
>>> Predicate(0, 0, 1).name # For compatibility only
(0, 0, 1)

property refs: Set[tuple | str]

References used to create indexes for predicate stores.

Attribute	Example	Description
`bicoords`	`(1, 0)`	symbol coordinates (index, subscript)
`spec`	`(1, 0, 2)`	coordinates including arity
`ident`	`('Predicate', (1, 0, 2))`	full lexical identifier
`name`	"Identity"	(system predicates only)

Constant 

class Constant[source]

Bases: Parameter

A constant is specified by an integer 2-tuple of (index, subscript). The index can range from 0-3, and the subscript can be any positive integer.

To create a constant, the spec can be passed either as separate arguments, or as a single tuple:

>>> c = Constant(2, 9)
>>> c == Constant((2, 9))
True

Behaviors

A constant can be right-shifted >> into a Quantified sentence as a convenience for the sentence's unquantify() method:

>>> c = Constant(0, 0)
>>> s1 = Quantified.first()
>>> s2 = c >> s1
>>> s2.constants == {c}
True

Variable 

class Variable[source]

Bases: Parameter

A variable, just like a Constant, is specified by an integer 2-tuple of (index, subscript). The index can range from 0-3, and the subscript can be any positive integer.

>>> Variable(2, 10) == Variable((2, 10))
True

Operator 

class Operator[source]

Bases: LexicalEnum

Operator enum class.

Behaviors

Calling an operator constructs an Operated sentence

>>> s1 = Atomic(0, 0)
>>> s2 = Operator.Conditional(s1, s1)
>>> s2 == Operated(Operator.Conditional, (s1, s1))
True

Some operators map to Python operators, such as & or ~.

>>> s = Atomic(0, 0)
>>> Operator.Conjunction(s, s) == s & s
True
>>> s.negate() == ~s
True

See the Sentence class for more.

Members

name	arity
Assertion	1
Negation	1
Conjunction	2
Disjunction	2
MaterialConditional	2
MaterialBiconditional	2
Conditional	2
Biconditional	2
Possibility	1
Necessity	1

arity: int: The operator arity.

Parameters:: value (object) --
Return type:: _EnumT

Quantifier 

class Quantifier[source]

Bases: LexicalEnum

Quantifier enum class.

Behaviors

Calling a quantifier constructs a Quantified sentence

>>> x = Variable(0, 0)
>>> s1 = Predicated.first()
>>> s2 = Quantifier.Existential(x, s1)
>>> s2 == Quantified(Quantifier.Existential, x, s1)
True

Existential: The ∃ Existential quantifier

Universal: The ∀ Universal quantifier

Parameters:: value (object) --
Return type:: _EnumT

Atomic 

class Atomic[source]

Bases: CoordsItem, Sentence

An atomic sentence sentence, like a Parameter, is specified by an integer 2-tuple of (index, subscript). The index can range from 0-4, and the subscript can be any positive integer.

>>> Atomic(4, 0) == Atomic((4, 0))
True

Predicated 

class Predicated[source]

Bases: Sentence, Sequence[Parameter]

Predicated sentence implementation.

__init__(pred, *params)[source]

Parameters:

pred (Predicate) -- The Predicate, or spec, such as (1, 0, 2).
params (Parameter) -- An iterable of Parameter

Raises:

TypeError -- if the number of params does not equal the predicate's arity.

predicate: Predicate: The predicate.

params: tuple[Parameter, ...]: The parameters.

classmethod first(pred=None, /)[source]

Parameters:: pred (Predicate) -- The Predicate or spec. Default is the Predicate.first().

Quantified 

class Quantified[source]

Bases: Sentence, Sequence

Quantified sentence implementation.

__init__(q, v, s, /)[source]

Parameters:

q (Quantifier) -- The Quantifier or name, such as "Existential".
v (Variable) -- The Variable to bind, or coords, such as (0, 0).
s (Sentence) -- The inner Sentence.

quantifier: Quantifier: The quantifier.

variable: Variable: The bound variable.

sentence: Sentence: The inner sentence.

items: tuple[Quantifier, Variable, Sentence]

Quantifer, Variable, Sentence.

Type:: The items sequence

unquantify(c, /)[source]

Instantiate the variable with a constant.

Parameters:: c (Constant) -- The constant to substitute for the bound variable.
Returns:: The unquantified sentence.
Return type:: Sentence

classmethod first(q=Quantifier.Existential, /)[source]

Parameters:: q (Quantifier) -- The quantifier, default is the first quantifier.

next(**sentkw)[source]

Keyword Arguments:: **sentkw -- kwargs for Sentence.next() to create the inner sentence.
Raises:: TypeError -- if Sentence.next() returns a sentence for which the variable is no longer bound.

Operated 

class Operated[source]

Bases: Sentence, Sequence[Sentence]

Operated sentence implementation.

__init__(oper, *operands)[source]

Parameters:

oper (Operator) -- The operator.
operands -- The operands.

operator: Operator: The operator.

operands: tuple[Sentence, ...]: The operands.

lhs: Sentence: The first (left-most) operand.

rhs: Sentence: The last (right-most) operand.

Collection Classes 

Argument 

class Argument[source]

Argument class.

A container of sentences (premises, conclusion) with sequence implementation, ordering and hashing.

Two arguments are considered equal just when their conclusions are equal, and their premises are equal (and in the same order). The title is not considered in equality.

Parameters:

conclusion (Sentence) --
premises (tuple[Sentence, ...]) --
title (str | None) --

Return type:

Argument

__init__(conclusion, premises=None, *, title=None)[source]

Parameters:

conclusion (Sentence) -- The conclusion.
premises (Iterable[Sentence | None]) -- The premises or None.
title (str | None) --

Keyword Arguments:

title -- An optional title.

premises: tuple[Sentence, ...]: The argument's premises

title: str | None: Optional title

property conclusion: Sentence: The argument's conclusion.

property hash: int: The argument's hash.

predicates(**kw)[source]

Return the predicates occuring in the argument.

Keyword Arguments:: **kw -- sort keywords to pass to Predicates constructor.
Returns:: The predicates.
Return type:: Predicates

argstr()[source]

Get the canonical string representation for recreating with from_argstr().

Returns:: The argument string.
Return type:: str

static from_argstr(argstr, /, *, title=None)[source]

Construct an argument from the canonical string representation from argstr().

Parameters:

argstr (str) -- The input string.
title (str | None) --

Keyword Arguments:

title (str) -- An optional title.

Returns:

The argument.

Return type:

Argument

Raises:

ParseError --
TypeError --

Predicates 

class Predicates[source]

Bases: PredicatesBase, qset[Predicate]

Predicate store. A sequenced set with a multi-keyed lookup index.

Predicates with the same symbol coordinates (index, subscript) may have different arities. This class ensures that conflicting predicates are not in the same set, which is necessary, for example, for determinate parsing.

__init__(values=None, /, *, sort=False, key=None, reverse=False)[source]

Create a new store from an iterable of predicate objects or specs

Parameters:

values -- Iterable of predicates or specs.

Keyword Arguments:

sort -- Whether to sort. Default is False.
key -- Optional sort key function.
reverse -- Whether to reverse sort.

get(ref, /, default=<object object>)

Get a predicate by any reference. Also searches system predicates.

Parameters:

ref -- Predicate reference. See Predicate.ref.
default -- Value to return if not found.

Returns:

The Predicate instance.

Raises:

KeyError -- if missing and no default specified.

Return type:

Predicate

Parser Classes 

Parser 

class Parser(notation: Notation | None = None, predicates: Predicates | None = None, table: ParseTable | str | None = None, **opts)[source]

Parser interface and coordinator.

To create a parser:

>>> from pytableaux.lang import Parser
>>> Parser()
<PolishParser:(<Notation.polish>, 'default')>
>>> Parser('standard')
<StandardParser:(<Notation.standard>, 'default')>

Or use the Notation enum class:

>>> from pytableaux.lang import Notation
>>> Parser(Notation.standard)
<StandardParser:(<Notation.standard>, 'default')>
>>> Notation.polish.Parser()
<PolishParser:(<Notation.polish>, 'default')>

To parse Predicated sentences, the parser must know the predicate's arity. By default, it will deduce the arity from the first usage.

>>> parser = Parser(notation='standard')
>>> parser('Fa & Gab')
<Sentence: Fa ∧ Gab>
>>> parser.predicates
Predicates({<Predicate: F>, <Predicate: G>})
>>> # parser('Fab') # raises ParseError

Alternatively, pass a Predicates object with the predicates:

>>> from pytableaux.lang import Predicates
>>> preds = Predicates(((0, 0, 1), (1, 0, 2)))
>>> parser = Parser('standard', preds, auto_preds=False)
>>> parser('Fa & Gab')
<Sentence: Fa ∧ Gab>

Return type:: Parser

abstract __call__(input, /)[source]

Parse a sentence from an input string.

Parameters:: input (str) -- The input string.
Returns:: The parsed sentence.
Return type:: Sentence
Raises:: ParseError --

argument(conclusion, premises=None, *, title=None)[source]

Parse the input strings and create an argument.

Parameters:

conclusion (str) -- The argument's conclusion.
premises (Iterable[str]) -- Premise strings, if any.
title (str | None) --

Keyword Arguments:

title -- An optional title.

Returns:

The argument.

Raises:

ParseError -- if input cannot be parsed.
TypeError -- for bad argument types.

Return type:

Argument

class DefaultParser[source]

Bases: Parser

Parser default implementation.

Return type:: Parser

class PolishParser[source]

Bases: DefaultParser

Polish notation parser.

Return type:: Parser

class StandardParser[source]

Bases: DefaultParser

Standard notation parser.

Options:: drop_parens: Don't require parentheses on all binary sentences. Default True.

Return type:: Parser

Writer Classes 

LexWriter 

class LexWriter(*args, **kw)[source]

LexWriter interface and coordinator.

__call__(item)[source]

Write a lexical item.

Parameters:: item (Lexical) -- The item to write.
Returns:: The rendered string.
Return type:: str

canwrite(obj)[source]

Whether the object can be written.

Parameters:: obj (Any) -- The object to test.
Returns:: Whether the object can be written.
Return type:: bool

class PolishLexWriter[source]

Bases: LexWriter

Polish notation lexical writer implementation.

class StandardLexWriter[source]

Bases: LexWriter

Standard notation lexical writer implementation.

Options:: drop_parens: Drop outer parens, default True. identity_infix: Write identity sentences in infix notation (e.g. a = b), default True. max_infix: The max arity for writing predicate sentences in infix notation, default 0.

Utility Classes 

class LexType[source]

LexType metadata enum class for concrete types.

name	rank	cls	role	maxi	pcls
Predicate	10	`Predicate`	`Predicate`	3	`Predicated`
Constant	20	`Constant`	`Parameter`	3	None
Variable	30	`Variable`	`Parameter`	3	None
Quantifier	40	`Quantifier`	`Quantifier`	None	`Quantified`
Operator	50	`Operator`	`Operator`	None	`Operated`
Atomic	60	`Atomic`	`Sentence`	4	None
Predicated	70	`Predicated`	`Sentence`	None	`Predicate`
Quantified	80	`Quantified`	`Sentence`	None	`Quantifier`
Operated	90	`Operated`	`Sentence`	None	`Operator`

Parameters:: value (object) --
Return type:: _EnumT

rank: int: A number to order items of different types.

cls: type[Lexical]: The class reference.

role: type[Lexical]: The category class, such as Sentence for Atomic.

maxi: int | None: For coordinate classes, the maximum index, else None.

pcls: type[Lexical] | None: The "partner" class, if any. For example, Operated and Operator are partners.

hash: int: The member hash.

classes: ClassVar[qsetf[type[Lexical]]]

Ordered set of all the classes.

class ParseTable[source]

Bases: MapCover[str, Any]

Parser table data class.

Parameters:: data (Mapping) --

classmethod load(data, /)[source]

Create and store instance from data.

Parameters:: data (Mapping) -- The data mapping
Raises:: Emsg.DuplicateKey -- on duplicate key
Returns:: The instance
Return type:: Self

classmethod fetch(notation, dialect=None)[source]

Get a loaded instance.

Parameters:

notation (Notation) -- The notation
dialect (str) -- The dialect. Default is 'default'.

Returns:

The instance

Return type:

Self

reversed: Mapping: Reversed mapping of item to symbol.

class StringTable(data, /)[source]

Bases: MapCover[Any, str]

Lexical writer strings table data class.

Parameters:: data (Mapping) --

classmethod load(data, /)[source]

Create and store instance from data.

Parameters:: data (Mapping) -- The data mapping
Raises:: Emsg.DuplicateKey -- on duplicate key
Returns:: The instance
Return type:: Self

classmethod fetch(format, notation, dialect=None)[source]

Get a loaded instance.

Parameters:

format (str) -- The format.
notation (Notation) -- The notation
dialect (str) -- The dialect if any.

Returns:

The instance

Return type:

Self

format: str: The format (html, latex, text, rst, etc.)

notation: Notation: The notation

dialect: str: The specific dialect, if any. Defaults to the name of the format.

class Notation(value, names=None, **kw)[source]

Notation (polish/standard) enum class.

name
polish
standard

Parameters:: value (object) --
Return type:: _EnumT

Parser: type[Parser]: The notation's parser class.

formats: dict[str, set[str]]: Mapping from format to dialects.

writers: set[type[LexWriter]]: All writer classes for the notation.

DefaultWriter: type[LexWriter]: The notations's default writer class.

classmethod get_common_formats()[source]

Get formats common to all notations.

Return type:: list[str]

class Marking(value, names=None, **kw)[source]

Miscellaneous marking/punctuation enum.

name
paren_open
paren_close
whitespace
digit
meta
subscript
subscript_open
subscript_close
tableau

Parameters:: value (object) --
Return type:: _EnumT

class BiCoords(index, subscript)[source]

An (index, subscript) integer tuple.

Parameters:

index (int) --
subscript (int) --

index: int: The index integer.

subscript: int: The subscript integer.

class Sorting(subscript, index)[source]

BiCoords sorting tuple (subscript, index).

Parameters:

subscript (int) --
index (int) --

subscript: int: The subscript integer.

index: int: The index integer.

sorting()[source]: Return the sorting tuple.

class TriCoords(index, subscript, arity)[source]

An (index, subscript, arity) integer tuple.

Parameters:

index (int) --
subscript (int) --
arity (int) --

index: int: The index integer.

subscript: int: The subscript integer.

arity: int: The arity integer.

class Sorting(subscript, index, arity)[source]

TriCoords sorting tuple (subscript, index, arity).

Parameters:

subscript (int) --
index (int) --
arity (int) --

subscript: int: The subscript integer.

index: int: The index integer.

arity: int: The arity integer.

sorting()[source]: Return the sorting tuple.