autstr.symbolic package

autstr.symbolic package#

Submodules#

autstr.symbolic.backends module#

Evaluation targets for compiled symbolic queries.

A backend knows how to answer a first-order query, what a relation’s arity is, and how to move between element encodings and automaton tapes. Everything above this module is backend-agnostic, which is what lets one expression language serve both a single structure and a whole uniformly automatic class.

class autstr.symbolic.backends.Backend[source]#

Bases: object

The interface a SymbolicContext evaluates against.

relation_symbols()[source]#

Return type:: List[str]

arity(symbol)[source]#

Arity of a relation symbol, or None if it is unknown here.

Return type:: Optional[int]
Parameters:: symbol (str)

arity_of(dfa)[source]#

Relation arity of an automaton produced by this backend.

Return type:: int

evaluate(expression, updates, prepared)[source]#

Answer a query. Returns (dfa, tape names).

Parameters:

updates (Dict)
prepared (Dict)

constant_automaton(word)[source]#

Parameters:: word (Sequence)

longer_witness_automaton(k, references)[source]#

Parameters:

k (int)
references (int)

accepts(dfa, values, codec)[source]#

Return type:: bool
Parameters:: values (Sequence)

iterate(dfa, codec, arity)[source]#

Parameters:: arity (int)

is_finite(dfa)[source]#

Whether the relation holds of finitely many tuples.

Return type:: bool

reserved_variable_names()[source]#

Variable names this backend cannot represent.

Return type:: set

check_member(expression, advice, assignments, implicit)[source]#

evaluate_member(expression, advice, assignments)[source]#

get_structure(advice)[source]#

describe()[source]#

Return type:: str

class autstr.symbolic.backends.StructureBackend(presentation)[source]#

Bases: Backend

Queries answered by an AutomaticPresentation.

relation_symbols()[source]#

arity(symbol)[source]#: Arity of a relation symbol, or None if it is unknown here.

arity_of(dfa)[source]#: Relation arity of an automaton produced by this backend.

evaluate(expression, updates, prepared)[source]#: Answer a query. Returns (dfa, tape names).

constant_automaton(word)[source]#

longer_witness_automaton(k, references)[source]#

accepts(dfa, values, codec)[source]#

iterate(dfa, codec, arity)[source]#

is_finite(dfa)[source]#: Whether the relation holds of finitely many tuples.

describe()[source]#

class autstr.symbolic.backends.TreeStructureBackend(presentation)[source]#

Bases: Backend

Queries answered by a TreeAutomaticPresentation.

Elements are trees rather than words, so a signature’s codec encodes Python values to Tree objects; everything above this module is unchanged, since the codec’s output is only ever handed back to the backend.

Every operation of the string backends is available; the ones whose string formulation counts word positions – enumeration order and exinf – are restated in terms of node count and path depth.

relation_symbols()[source]#

arity(symbol)[source]#: Arity of a relation symbol, or None if it is unknown here.

arity_of(sta)[source]#: Relation arity of an automaton produced by this backend.

evaluate(expression, updates, prepared)[source]#: Answer a query. Returns (dfa, tape names).

constant_automaton(tree)[source]#

longer_witness_automaton(k, references)[source]#

accepts(sta, values, codec)[source]#

iterate(sta, codec, arity)[source]#

is_finite(sta)[source]#: Whether the relation holds of finitely many tuples.

describe()[source]#

class autstr.symbolic.backends.ClassBackend(klass)[source]#

Bases: Backend

Queries answered by a UniformlyAutomaticClass.

Formulas are written over the class signature exactly as for a single structure; the advice tape is added and quantifiers are relativized to the member domain by the class’s own evaluator. The advice appears in results under the reserved tape name 'advice'.

ADVICE = 'advice'#

relation_symbols()[source]#

arity(symbol)[source]#: Arity of a relation symbol, or None if it is unknown here.

arity_of(dfa)[source]#: Relation arity of an automaton produced by this backend.

evaluate(expression, updates, prepared)[source]#: Answer a query. Returns (dfa, tape names).

reserved_variable_names()[source]#: Variable names this backend cannot represent.

constant_automaton(word)[source]#

longer_witness_automaton(k, references)[source]#

accepts(dfa, values, codec)[source]#

iterate(dfa, codec, arity)[source]#

is_finite(dfa)[source]#: Whether the relation holds of finitely many tuples.

check_member(expression, advice, assignments, implicit)[source]#

evaluate_member(expression, advice, assignments)[source]#

get_structure(advice)[source]#

describe()[source]#

autstr.symbolic.compiler module#

Compilation of symbolic expressions into first-order queries.

The output is an nltk expression plus a table of automata to splice in, which is exactly what every evaluation backend in the package already consumes – AutomaticPresentation._build_automaton, the relativizing class evaluator, and the implicit engine. The symbolic layer is a frontend, not a fourth engine.

Two things happen here that the string-formula approach could not do safely:

Variable renaming. nltk only recognizes an argument as an individual variable if its name matches [a-df-z][0-9]*; anything else – foo, x_1, e – is silently reclassified and drops out of the free-variable list, which corrupts tape order rather than raising. User-chosen names are therefore mangled to legal ones on the way in and restored on the way out. Free variables are numbered in sorted order with a fixed width, so the lexicographic order the engine uses to lay out tapes agrees with the sorted order of the user’s names.

Term flattening. An atom R(f(x), y) becomes exists w.(Graph_f(x, w) and R(w, y)). Witnesses are introduced once per distinct subterm within an atom, and they are quantified at the atom rather than hoisted, so a partial function’s graph keeps its meaning under negation.

autstr.symbolic.compiler.FREE_PREFIX = 'a'#: Prefixes for the three kinds of generated names. All are legal nltk individual-variable initials, and the groups are disjoint by construction.

exception autstr.symbolic.compiler.CompileError[source]#: Bases: Exception

class autstr.symbolic.compiler.Compiler(ctx)[source]#

Bases: object

Lowers one symbolic formula. Instantiate per compilation – it carries the name allocator and the automata collected along the way.

updates: Dict[str, object]#

prepared: Dict[str, object]#

compile(formula)[source]#

Returns (nltk expression, free variable names in tape order).

Parameters:: formula (Formula)

property names: _Names#

arity(symbol)[source]#

Return type:: int
Parameters:: symbol (str)

autstr.symbolic.compiler.restore(names, internal)[source]#

Map internal tape names back to the user’s variable names.

Return type:

List[str]

Parameters:

names (_Names)
internal (Sequence[str])

autstr.symbolic.context module#

Binding a signature to a structure: the user-facing symbolic interface.

A SymbolicContext is what AutomaticPresentation.symbolic() and UniformlyAutomaticClass.symbolic() hand back. It mints variables, relation and function symbols, and evaluates the expressions built from them against its backend.

exception autstr.symbolic.context.SymbolicSymbolError[source]#: Bases: Exception

class autstr.symbolic.context.RelationSymbol(ctx, symbol)[source]#

Bases: object

A relation symbol of the signature, applied to build atoms.

Parameters:: symbol (str)

property arity: int#

class autstr.symbolic.context.FunctionSymbol(ctx, name, function)[source]#

Bases: object

A function symbol of the signature, applied to build terms.

Parameters:

name (str)
function (Function)

property arity: int#

class autstr.symbolic.context.SymbolicContext(backend, signature=None)[source]#

Bases: object

The symbolic interface to one structure or one class of structures.

Parameters:

backend – evaluation target (see autstr.symbolic.backends).
signature (Optional[Signature]) – declared functions, operators and codec. Relation arities are read from the backend’s automata.

var(name)[source]#

A single symbolic variable. Any non-empty name works – names are renamed to legal ones during compilation and restored in results.

Return type:: Var
Parameters:: name (str)

vars(names)[source]#

Several symbolic variables. Accepts a list of names or a single whitespace-separated string.

Return type:: tuple
Parameters:: names (str | Sequence[str])

get_symbolic_vars(names)#

Several symbolic variables. Accepts a list of names or a single whitespace-separated string.

Return type:: tuple
Parameters:: names (str | Sequence[str])

const(value)[source]#

A constant term for a Python value, encoded through the codec.

Return type:: Const

term(x)[source]#

Coerce a variable name, Python value or term into a term.

Return type:: Term

rel(symbol)[source]#

A relation symbol of the signature.

Return type:: RelationSymbol
Parameters:: symbol (str)

get_symbolic_rel(symbol)#

A relation symbol of the signature.

Return type:: RelationSymbol
Parameters:: symbol (str)

func(name)[source]#

A function symbol of the signature.

Return type:: FunctionSymbol
Parameters:: name (str)

get_symbolic_func(name)#

A function symbol of the signature.

Return type:: FunctionSymbol
Parameters:: name (str)

atom(symbol, args)[source]#

The atom symbol(*args).

Return type:: Formula
Parameters:: symbol (str)

relation(dfa, args, label='given')[source]#

An atom backed by an automaton built outside the symbolic layer.

Return type:: Formula
Parameters:: label (str)

relation_arity(symbol)[source]#

Return type:: int
Parameters:: symbol (str)

function(name)[source]#

Return type:: Function
Parameters:: name (str)

symbols()[source]#

A summary of what this context offers.

Return type:: Dict[str, List[str]]

describe()[source]#

Return type:: str

fresh_name(taken)[source]#

A user-level variable name not in taken.

Return type:: str

compile(formula)[source]#

The first-order query this formula lowers to. Returned as (expression, variables) with variables naming the tapes in the user’s own vocabulary – useful for inspection and debugging.

Parameters:: formula (Formula)

evaluate(formula)[source]#

Compile and evaluate, returning the presentation of the satisfying assignments together with its tape order.

Return type:: Relation
Parameters:: formula (Formula)

check(formula)[source]#

True if the formula is satisfiable over the structure – free variables read as existentially quantified.

Return type:: bool
Parameters:: formula (Formula)

check_member(formula, advice, implicit=False, **assignments)[source]#

Model check a formula against the member structure picked out by advice.

Parameters:

advice – the advice string identifying the member.
implicit (bool) – evaluate on the fly over the base automata instead of compiling a query automaton – the same trade-off as UniformlyAutomaticClass.check_implicit, and the only route for classes whose query automaton is infeasible to build.
assignments – concrete elements for free variables, named by the variables of this expression. Unassigned free variables are read as existentially quantified.
formula (Formula)

Return type:

bool

evaluate_member(formula, advice, **assignments)[source]#

The satisfying set of a formula on one member, computed implicitly.

Returns a solution set that knows its exact size without enumerating and yields assignments lazily; see autstr.implicit.

Parameters:: formula (Formula)

get_structure(advice)[source]#: The member structure for advice as an ordinary automatic presentation. Call symbolic on it to work inside that one member.

materialize(formula, name=None)[source]#

Evaluate now, and return a formula that splices the result in.

Return type:

Formula

Parameters:

formula (Formula)
name (str)

class autstr.symbolic.context.Relation(ctx, dfa, variables)[source]#

Bases: object

The result of evaluating a formula: an automaton plus the tape order.

The tape order is the sorted list of the formula’s free variable names. Membership and iteration are keyed by name, never by position, so renaming a variable cannot silently change what a query means.

Parameters:

ctx (SymbolicContext)
variables (Sequence[str])

property arity: int#

is_empty()[source]#

Return type:: bool

is_finite()[source]#

Whether finitely many tuples satisfy the relation.

Return type:: bool

reorder(variables)[source]#

The same relation with its tapes permuted into the given order.

Return type:: Relation
Parameters:: variables (Sequence[str])

contains(*positional, **assignment)[source]#

Whether a tuple satisfies the relation. Positional arguments follow variables; keyword arguments name them.

Return type:: bool

autstr.symbolic.expr module#

The symbolic expression AST.

Terms denote elements of a structure, formulas denote relations over it. Nodes are immutable and compare structurally, so equal subexpressions are interchangeable and can be used as dictionary keys. Nothing here touches an automaton: building an expression is pure bookkeeping, and all automata construction happens when the expression is handed to a backend (see autstr.symbolic.compiler).

Operators are not hardwired. x + y looks up '+' in the structure’s Signature.operators and builds an application of whatever function symbol it names; a structure that declares no '+' raises a clear error instead of silently meaning addition.

class autstr.symbolic.expr.Node(ctx, key)[source]#

Bases: object

Common base: immutable, structurally compared, bound to a context.

Parameters:: key (tuple)

ctx#

class autstr.symbolic.expr.Term(ctx, key)[source]#

Bases: Node

A term denoting an element of the structure.

Parameters:: key (tuple)

variables()[source]#

Free variable names, sorted.

Return type:: List[str]

eq(other)[source]#

The relation self = other, via the structure’s equality relation.

Return type:: Formula

rel(symbol, *others)[source]#

The atom symbol(self, *others).

Return type:: Formula
Parameters:: symbol (str)

times(n)[source]#

The n-fold sum self + ... + self under the structure’s '+', built by base-2 decomposition so that only \(O(\log_2 n)\) distinct subterms are created.

Negative n requires the structure to declare a '-' inverse.

Return type:: Term
Parameters:: n (int)

substitute(**replacements)[source]#

Replace free variables. Terms are immutable, so this returns a new term and never disturbs expressions that share this one.

Return type:: Term

class autstr.symbolic.expr.Var(ctx, name)[source]#

Bases: Term

A free variable.

Parameters:: name (str)

variables()[source]#: Free variable names, sorted.

name#

class autstr.symbolic.expr.Const(ctx, value)[source]#

Bases: Term

A Python value, encoded through the signature’s codec.

variables()[source]#: Free variable names, sorted.

value#

class autstr.symbolic.expr.Apply(ctx, func, args)[source]#

Bases: Term

An application f(t_1, ..., t_n) of a declared function symbol.

Parameters:

func (str)
args (Sequence[Term])

variables()[source]#: Free variable names, sorted.

func#

args#

class autstr.symbolic.expr.Formula(ctx, key)[source]#

Bases: Node

A formula denoting a relation over the structure.

Parameters:: key (tuple)

variables()[source]#

Free variable names, sorted. This is also the tape order of the automaton produced by evaluate.

Return type:: List[str]

implies(other)[source]#

Return type:: Formula

iff(other)[source]#

Return type:: Formula

drop(variables)[source]#

Project the relation away from variables – equivalently, existentially quantify them.

Return type:: Formula

ex(variables)#

Project the relation away from variables – equivalently, existentially quantify them.

Return type:: Formula

all(variables)[source]#

Universally quantify variables.

Return type:: Formula

exinf(variable)[source]#

\(\exists^\infty\) – the tuples extended by infinitely many witnesses for variable.

Return type:: Formula

substitute(**replacements)[source]#

Replace free variables, avoiding capture by bound variables.

Return type:: Formula

evaluate()[source]#: Compile to a Relation: the presentation of the satisfying assignments together with its tape order.

check()[source]#

True if the relation is non-empty (free variables read as existentially quantified).

Return type:: bool

is_empty()[source]#

Return type:: bool

is_finite()[source]#

Return type:: bool

contains(*args, **assignment)[source]#

Return type:: bool

materialize(name=None)[source]#

Evaluate now and return a formula standing for the resulting automaton. Use it to share an expensive subformula across queries; the compiled automaton is spliced in instead of being rebuilt.

Parameters:: name (str)

class autstr.symbolic.expr.Atom(ctx, symbol, args)[source]#

Bases: Formula

R(t_1, ..., t_n) for a relation symbol of the signature.

Parameters:

symbol (str)
args (Sequence[Term])

variables()[source]#: Free variable names, sorted. This is also the tape order of the automaton produced by evaluate.

symbol#

args#

class autstr.symbolic.expr.DfaAtom(ctx, dfa, args, label='anon', prepared=False)[source]#

Bases: Formula

An atom backed by an automaton supplied directly rather than by a signature symbol – the splice point for Formula.materialize and for automata built outside the symbolic layer.

Parameters:

args (Sequence[Term])
label (str)
prepared (bool)

variables()[source]#: Free variable names, sorted. This is also the tape order of the automaton produced by evaluate.

dfa#

args#

label#

prepared#

class autstr.symbolic.expr.Not(ctx, body)[source]#

Bases: Formula

Parameters:: body (Formula)

variables()[source]#: Free variable names, sorted. This is also the tape order of the automaton produced by evaluate.

body#

class autstr.symbolic.expr.And(ctx, left, right)[source]#

Bases: _Binary

Parameters:

left (Formula)
right (Formula)

connective = 'and'#

class autstr.symbolic.expr.Or(ctx, left, right)[source]#

Bases: _Binary

Parameters:

left (Formula)
right (Formula)

connective = 'or'#

class autstr.symbolic.expr.Exists(ctx, bound, body)[source]#

Bases: _Quantifier

Parameters:

bound (Sequence[str])
body (Formula)

keyword = 'exists'#

class autstr.symbolic.expr.Forall(ctx, bound, body)[source]#

Bases: _Quantifier

Parameters:

bound (Sequence[str])
body (Formula)

keyword = 'forall'#

class autstr.symbolic.expr.ExInf(ctx, variable, body)[source]#

Bases: Formula

\(\exists^\infty x. \varphi\).

Parameters:

variable (str)
body (Formula)

variables()[source]#: Free variable names, sorted. This is also the tape order of the automaton produced by evaluate.

variable#

body#

autstr.symbolic.expr.all_names(node)[source]#

Every variable name occurring in a formula, free or bound.

Return type:: set

autstr.symbolic.signature module#

Signatures: what a structure exposes to the symbolic layer.

An automatic presentation is a bag of automata keyed by relation symbol. A signature adds the information the symbolic layer needs on top of that: which relations are graphs of functions, which Python operators those functions are bound to, and how Python values translate to and from element encodings.

Arities are never declared – they are read off the automata themselves (dfa.symbol_arity, minus the advice tape for a uniformly automatic class).

class autstr.symbolic.signature.Function(graph, out=-1)[source]#

Bases: object

A function symbol, presented by the automaton of its graph.

Parameters:

graph (str) – relation symbol whose automaton recognizes the graph.
out (int) – position of the output tape in the graph relation. Defaults to the last tape; negative values count from the end.
arity – number of inputs. Derived from the graph relation’s arity when the signature is bound to a structure.

graph: str#

out: int = -1#

positions(graph_arity)[source]#

(input positions in order, output position) for a graph of the given arity.

Return type:: tuple
Parameters:: graph_arity (int)

autstr.symbolic.signature.EQUALITY_SYMBOL = 'Eq'#: The standard name for a structure’s equality relation. Some structures also answer to ‘E’, but ‘E’ is the edge relation in every graph class, so equality is always named explicitly rather than guessed from the symbols.

autstr.symbolic.signature.operation_signature(relations, graph, operator, equality='Eq', codec=None)[source]#

The signature of a structure whose binary operation is presented by the ternary graph relation graph, bound to operator.

Equality is bound to .eq when the structure declares equality. The name is passed in rather than guessed: ‘E’ means equality in Skolem arithmetic but the edge relation in every graph class, so guessing would silently answer “are these adjacent?” for “are these equal?”.

A structure without an equality relation still gets the operator, but its terms cannot become formulas – (x + y).eq(z) is the only way to say what a term denotes.

Parameters:

relations – the structure’s relation symbols.
graph (str) – the ternary relation R(x, y, z) meaning x op y = z.
operator (str) – the Python operator to bind, '*' or '+'.
codec – optional element codec; unused over a uniformly automatic class, where an element’s encoding depends on the advice.
equality (str)

Return type:

Signature

autstr.symbolic.signature.relational_signature(relations, methods, equality='Eq', codec=None)[source]#

The signature of a purely relational structure: each method name in methods bound to the relation symbol it names, plus equality when the structure declares it.

Nothing binds to + or * — a relational structure carries no operation, so every symbol is reached as a method, exactly like .lt in the arithmetic signature. The requested methods are bound whether or not the structure declares them, so a symbol that is missing fails loudly when a formula uses it rather than silently going unbound; only equality, which a caller asks for generically, is conditional.

Parameters:

relations – the structure’s relation symbols.
methods (Dict[str, str]) – {method name: relation symbol}.
equality (str) – the equality symbol, bound to .eq when present.
codec – optional element codec for writing elements as constants.

Return type:

Signature

autstr.symbolic.signature.graph_signature(relations, edge='E', adjacency='adj', equality='Eq', codec=None)[source]#

The signature of a graph: the binary edge relation edge bound to the method .{adjacency}(y) (default .adj), plus equality when the structure declares it.

A graph carries no operation, so nothing binds to + or *; adjacency is a relation method, exactly like .lt in the arithmetic signature. The edge name is passed in, never guessed — E means the edge here but equality elsewhere, the same hazard operation_signature guards against.

Parameters:

relations – the structure’s relation symbols.
edge (str) – the binary relation read as adjacency.
adjacency (str) – the method name it binds to.
codec – optional element codec for writing vertices as constants.
equality (str)

Return type:

Signature

autstr.symbolic.signature.order_signature(relations, less='Lt', order='lt', equality='Eq', codec=None, methods=None)[source]#

The signature of an ordered structure: the binary relation less bound to .{order}(y) (default .lt), plus equality when declared.

An order is not a graph — x.lt(y) and x.adj(y) read differently even where both are binary — so orders get their own vocabulary rather than being wrapped as graphs. Further relations of the same structure (a successor, a limit predicate) go in methods.

Parameters:

relations – the structure’s relation symbols.
less (str) – the binary relation read as the strict order.
order (str) – the method name it binds to.
codec – optional element codec for writing elements as constants.
methods (Optional[Dict[str, str]]) – further {method name: relation symbol} bindings.
equality (str)

Return type:

Signature

class autstr.symbolic.signature.ElementCodec[source]#

Bases: object

Translation between Python values and element encodings.

What an encoding is belongs to the backend: a list of base-alphabet symbols in the order the automata read them for the string engines, a Tree for the tree engine. The codec’s output is only ever handed back to the backend that asked for it, so this layer does not interpret it.

Supplying a codec is optional: without one the symbolic layer still works, but constants cannot be written as Python values and solutions are yielded in their raw encoded form.

encode(value)[source]#

Return type:: Any
Parameters:: value (Any)

decode(encoded)[source]#

Return type:: Any
Parameters:: encoded (Any)

class autstr.symbolic.signature.FunctionCodec(encoder, decoder=None)[source]#

Bases: ElementCodec

A codec built from two plain functions.

Parameters:

encoder (Callable[[Any], Any])
decoder (Callable[[Any], Any] | None)

encoder: Callable[[Any], Any]#

decoder: Callable[[Any], Any] | None = None#

encode(value)[source]#

decode(word)[source]#

class autstr.symbolic.signature.Signature(functions=<factory>, operators=<factory>, codec=None, relations=<factory>)[source]#

Bases: object

The symbolic-layer description of a structure’s signature.

Parameters:

functions (Dict[str, Function]) – function symbol -> Function. The graph relation must exist in the presentation.
operators (Dict[str, str]) – Python operator or method name -> symbol it dispatches to. Keys may name a function symbol’s operator ('+', '-', '*', '@') or a relation method (any identifier, e.g. 'lt', 'eq'), and values are function or relation symbols respectively.
codec (Optional[ElementCodec]) – optional ElementCodec for constants and decoding.
relations (Dict[str, int]) – optional arity overrides. Normally arities come from the automata; entries here are only consulted for symbols that are not (yet) present in the presentation.

functions: Dict[str, Function]#

operators: Dict[str, str]#

codec: ElementCodec | None = None#

relations: Dict[str, int]#

function(name, graph, out=-1)[source]#

Declare a function symbol. Returns self, so declarations chain.

Return type:

Signature

Parameters:

name (str)
graph (str)
out (int)

operator(op, symbol)[source]#

Bind a Python operator or method name to a function or relation symbol. Returns self, so declarations chain.

Return type:

Signature

Parameters:

op (str)
symbol (str)

Module contents#

Symbolic first-order expressions over automatic structures and classes.

Instead of writing formula strings, build them from variables and symbols the structure hands out:

A = BuechiArithmeticZ()
S = A.symbolic()
x, y, z = S.vars("x y z")
phi = ((x + y).eq(z) & z.lt(10)).drop(y)

phi.check()            # satisfiable?
phi.evaluate()         # presentation of the satisfying assignments
(1, 5) in phi          # membership, by the sorted tape order
list(phi)              # enumerate solutions

The same expressions compile against a UniformlyAutomaticClass, where they define relations uniformly across every member structure.

Relation and function arities come from the automata; which relations are function graphs, which Python operators they are bound to, and how Python values encode as elements are declared in a Signature.

class autstr.symbolic.Backend[source]#

Bases: object

The interface a SymbolicContext evaluates against.

relation_symbols()[source]#

Return type:: List[str]

arity(symbol)[source]#

Arity of a relation symbol, or None if it is unknown here.

Return type:: Optional[int]
Parameters:: symbol (str)

arity_of(dfa)[source]#

Relation arity of an automaton produced by this backend.

Return type:: int

evaluate(expression, updates, prepared)[source]#

Answer a query. Returns (dfa, tape names).

Parameters:

updates (Dict)
prepared (Dict)

constant_automaton(word)[source]#

Parameters:: word (Sequence)

longer_witness_automaton(k, references)[source]#

Parameters:

k (int)
references (int)

accepts(dfa, values, codec)[source]#

Return type:: bool
Parameters:: values (Sequence)

iterate(dfa, codec, arity)[source]#

Parameters:: arity (int)

is_finite(dfa)[source]#

Whether the relation holds of finitely many tuples.

Return type:: bool

reserved_variable_names()[source]#

Variable names this backend cannot represent.

Return type:: set

check_member(expression, advice, assignments, implicit)[source]#

evaluate_member(expression, advice, assignments)[source]#

get_structure(advice)[source]#

describe()[source]#

Return type:: str

class autstr.symbolic.ClassBackend(klass)[source]#

Bases: Backend

Queries answered by a UniformlyAutomaticClass.

ADVICE = 'advice'#

relation_symbols()[source]#

arity(symbol)[source]#: Arity of a relation symbol, or None if it is unknown here.

arity_of(dfa)[source]#: Relation arity of an automaton produced by this backend.

evaluate(expression, updates, prepared)[source]#: Answer a query. Returns (dfa, tape names).

reserved_variable_names()[source]#: Variable names this backend cannot represent.

constant_automaton(word)[source]#

longer_witness_automaton(k, references)[source]#

accepts(dfa, values, codec)[source]#

iterate(dfa, codec, arity)[source]#

is_finite(dfa)[source]#: Whether the relation holds of finitely many tuples.

check_member(expression, advice, assignments, implicit)[source]#

evaluate_member(expression, advice, assignments)[source]#

get_structure(advice)[source]#

describe()[source]#

exception autstr.symbolic.CompileError[source]#: Bases: Exception

class autstr.symbolic.ElementCodec[source]#

Bases: object

Translation between Python values and element encodings.

Supplying a codec is optional: without one the symbolic layer still works, but constants cannot be written as Python values and solutions are yielded in their raw encoded form.

encode(value)[source]#

Return type:: Any
Parameters:: value (Any)

decode(encoded)[source]#

Return type:: Any
Parameters:: encoded (Any)

class autstr.symbolic.Formula(ctx, key)[source]#

Bases: Node

A formula denoting a relation over the structure.

Parameters:: key (tuple)

variables()[source]#

Free variable names, sorted. This is also the tape order of the automaton produced by evaluate.

Return type:: List[str]

implies(other)[source]#

Return type:: Formula

iff(other)[source]#

Return type:: Formula

drop(variables)[source]#

Project the relation away from variables – equivalently, existentially quantify them.

Return type:: Formula

ex(variables)#

Project the relation away from variables – equivalently, existentially quantify them.

Return type:: Formula

all(variables)[source]#

Universally quantify variables.

Return type:: Formula

exinf(variable)[source]#

\(\exists^\infty\) – the tuples extended by infinitely many witnesses for variable.

Return type:: Formula

substitute(**replacements)[source]#

Replace free variables, avoiding capture by bound variables.

Return type:: Formula

evaluate()[source]#: Compile to a Relation: the presentation of the satisfying assignments together with its tape order.

check()[source]#

True if the relation is non-empty (free variables read as existentially quantified).

Return type:: bool

is_empty()[source]#

Return type:: bool

is_finite()[source]#

Return type:: bool

contains(*args, **assignment)[source]#

Return type:: bool

materialize(name=None)[source]#

Evaluate now and return a formula standing for the resulting automaton. Use it to share an expensive subformula across queries; the compiled automaton is spliced in instead of being rebuilt.

Parameters:: name (str)

class autstr.symbolic.FunctionCodec(encoder, decoder=None)[source]#

Bases: ElementCodec

A codec built from two plain functions.

Parameters:

encoder (Callable[[Any], Any])
decoder (Callable[[Any], Any] | None)

encoder: Callable[[Any], Any]#

decoder: Callable[[Any], Any] | None = None#

encode(value)[source]#

decode(word)[source]#

class autstr.symbolic.FunctionSymbol(ctx, name, function)[source]#

Bases: object

A function symbol of the signature, applied to build terms.

Parameters:

name (str)
function (Function)

property arity: int#

class autstr.symbolic.Relation(ctx, dfa, variables)[source]#

Bases: object

The result of evaluating a formula: an automaton plus the tape order.

Parameters:

ctx (SymbolicContext)
variables (Sequence[str])

property arity: int#

is_empty()[source]#

Return type:: bool

is_finite()[source]#

Whether finitely many tuples satisfy the relation.

Return type:: bool

reorder(variables)[source]#

The same relation with its tapes permuted into the given order.

Return type:: Relation
Parameters:: variables (Sequence[str])

contains(*positional, **assignment)[source]#

Whether a tuple satisfies the relation. Positional arguments follow variables; keyword arguments name them.

Return type:: bool

class autstr.symbolic.RelationSymbol(ctx, symbol)[source]#

Bases: object

A relation symbol of the signature, applied to build atoms.

Parameters:: symbol (str)

property arity: int#

class autstr.symbolic.Signature(functions=<factory>, operators=<factory>, codec=None, relations=<factory>)[source]#

Bases: object

The symbolic-layer description of a structure’s signature.

Parameters:

functions (Dict[str, Function]) – function symbol -> Function. The graph relation must exist in the presentation.
operators (Dict[str, str]) – Python operator or method name -> symbol it dispatches to. Keys may name a function symbol’s operator ('+', '-', '*', '@') or a relation method (any identifier, e.g. 'lt', 'eq'), and values are function or relation symbols respectively.
codec (Optional[ElementCodec]) – optional ElementCodec for constants and decoding.
relations (Dict[str, int]) – optional arity overrides. Normally arities come from the automata; entries here are only consulted for symbols that are not (yet) present in the presentation.

functions: Dict[str, Function]#

operators: Dict[str, str]#

codec: ElementCodec | None = None#

relations: Dict[str, int]#

function(name, graph, out=-1)[source]#

Declare a function symbol. Returns self, so declarations chain.

Return type:

Signature

Parameters:

name (str)
graph (str)
out (int)

operator(op, symbol)[source]#

Bind a Python operator or method name to a function or relation symbol. Returns self, so declarations chain.

Return type:

Signature

Parameters:

op (str)
symbol (str)

class autstr.symbolic.StructureBackend(presentation)[source]#

Bases: Backend

Queries answered by an AutomaticPresentation.

relation_symbols()[source]#

arity(symbol)[source]#: Arity of a relation symbol, or None if it is unknown here.

arity_of(dfa)[source]#: Relation arity of an automaton produced by this backend.

evaluate(expression, updates, prepared)[source]#: Answer a query. Returns (dfa, tape names).

constant_automaton(word)[source]#

longer_witness_automaton(k, references)[source]#

accepts(dfa, values, codec)[source]#

iterate(dfa, codec, arity)[source]#

is_finite(dfa)[source]#: Whether the relation holds of finitely many tuples.

describe()[source]#

class autstr.symbolic.SymbolicContext(backend, signature=None)[source]#

Bases: object

The symbolic interface to one structure or one class of structures.

Parameters:

backend – evaluation target (see autstr.symbolic.backends).
signature (Optional[Signature]) – declared functions, operators and codec. Relation arities are read from the backend’s automata.

var(name)[source]#

A single symbolic variable. Any non-empty name works – names are renamed to legal ones during compilation and restored in results.

Return type:: Var
Parameters:: name (str)

vars(names)[source]#

Several symbolic variables. Accepts a list of names or a single whitespace-separated string.

Return type:: tuple
Parameters:: names (str | Sequence[str])

get_symbolic_vars(names)#

Several symbolic variables. Accepts a list of names or a single whitespace-separated string.

Return type:: tuple
Parameters:: names (str | Sequence[str])

const(value)[source]#

A constant term for a Python value, encoded through the codec.

Return type:: Const

term(x)[source]#

Coerce a variable name, Python value or term into a term.

Return type:: Term

rel(symbol)[source]#

A relation symbol of the signature.

Return type:: RelationSymbol
Parameters:: symbol (str)

get_symbolic_rel(symbol)#

A relation symbol of the signature.

Return type:: RelationSymbol
Parameters:: symbol (str)

func(name)[source]#

A function symbol of the signature.

Return type:: FunctionSymbol
Parameters:: name (str)

get_symbolic_func(name)#

A function symbol of the signature.

Return type:: FunctionSymbol
Parameters:: name (str)

atom(symbol, args)[source]#

The atom symbol(*args).

Return type:: Formula
Parameters:: symbol (str)

relation(dfa, args, label='given')[source]#

An atom backed by an automaton built outside the symbolic layer.

Return type:: Formula
Parameters:: label (str)

relation_arity(symbol)[source]#

Return type:: int
Parameters:: symbol (str)

function(name)[source]#

Return type:: Function
Parameters:: name (str)

symbols()[source]#

A summary of what this context offers.

Return type:: Dict[str, List[str]]

describe()[source]#

Return type:: str

fresh_name(taken)[source]#

A user-level variable name not in taken.

Return type:: str

compile(formula)[source]#

The first-order query this formula lowers to. Returned as (expression, variables) with variables naming the tapes in the user’s own vocabulary – useful for inspection and debugging.

Parameters:: formula (Formula)

evaluate(formula)[source]#

Compile and evaluate, returning the presentation of the satisfying assignments together with its tape order.

Return type:: Relation
Parameters:: formula (Formula)

check(formula)[source]#

True if the formula is satisfiable over the structure – free variables read as existentially quantified.

Return type:: bool
Parameters:: formula (Formula)

check_member(formula, advice, implicit=False, **assignments)[source]#

Model check a formula against the member structure picked out by advice.

Parameters:

advice – the advice string identifying the member.
implicit (bool) – evaluate on the fly over the base automata instead of compiling a query automaton – the same trade-off as UniformlyAutomaticClass.check_implicit, and the only route for classes whose query automaton is infeasible to build.
assignments – concrete elements for free variables, named by the variables of this expression. Unassigned free variables are read as existentially quantified.
formula (Formula)

Return type:

bool

evaluate_member(formula, advice, **assignments)[source]#

The satisfying set of a formula on one member, computed implicitly.

Returns a solution set that knows its exact size without enumerating and yields assignments lazily; see autstr.implicit.

Parameters:: formula (Formula)

get_structure(advice)[source]#: The member structure for advice as an ordinary automatic presentation. Call symbolic on it to work inside that one member.

materialize(formula, name=None)[source]#

Evaluate now, and return a formula that splices the result in.

Return type:

Formula

Parameters:

formula (Formula)
name (str)

exception autstr.symbolic.SymbolicSymbolError[source]#: Bases: Exception

class autstr.symbolic.Term(ctx, key)[source]#

Bases: Node

A term denoting an element of the structure.

Parameters:: key (tuple)

variables()[source]#

Free variable names, sorted.

Return type:: List[str]

eq(other)[source]#

The relation self = other, via the structure’s equality relation.

Return type:: Formula

rel(symbol, *others)[source]#

The atom symbol(self, *others).

Return type:: Formula
Parameters:: symbol (str)

times(n)[source]#

The n-fold sum self + ... + self under the structure’s '+', built by base-2 decomposition so that only \(O(\log_2 n)\) distinct subterms are created.

Negative n requires the structure to declare a '-' inverse.

Return type:: Term
Parameters:: n (int)

substitute(**replacements)[source]#

Replace free variables. Terms are immutable, so this returns a new term and never disturbs expressions that share this one.

Return type:: Term

class autstr.symbolic.Var(ctx, name)[source]#

Bases: Term

A free variable.

Parameters:: name (str)

variables()[source]#: Free variable names, sorted.

name#

autstr.symbolic.graph_signature(relations, edge='E', adjacency='adj', equality='Eq', codec=None)[source]#

The signature of a graph: the binary edge relation edge bound to the method .{adjacency}(y) (default .adj), plus equality when the structure declares it.

Parameters:

relations – the structure’s relation symbols.
edge (str) – the binary relation read as adjacency.
adjacency (str) – the method name it binds to.
codec – optional element codec for writing vertices as constants.
equality (str)

Return type:

Signature

autstr.symbolic.operation_signature(relations, graph, operator, equality='Eq', codec=None)[source]#

The signature of a structure whose binary operation is presented by the ternary graph relation graph, bound to operator.

A structure without an equality relation still gets the operator, but its terms cannot become formulas – (x + y).eq(z) is the only way to say what a term denotes.

Parameters:

relations – the structure’s relation symbols.
graph (str) – the ternary relation R(x, y, z) meaning x op y = z.
operator (str) – the Python operator to bind, '*' or '+'.
codec – optional element codec; unused over a uniformly automatic class, where an element’s encoding depends on the advice.
equality (str)

Return type:

Signature

autstr.symbolic.order_signature(relations, less='Lt', order='lt', equality='Eq', codec=None, methods=None)[source]#

The signature of an ordered structure: the binary relation less bound to .{order}(y) (default .lt), plus equality when declared.

Parameters:

relations – the structure’s relation symbols.
less (str) – the binary relation read as the strict order.
order (str) – the method name it binds to.
codec – optional element codec for writing elements as constants.
methods (Optional[Dict[str, str]]) – further {method name: relation symbol} bindings.
equality (str)

Return type:

Signature

autstr.symbolic.relational_signature(relations, methods, equality='Eq', codec=None)[source]#

The signature of a purely relational structure: each method name in methods bound to the relation symbol it names, plus equality when the structure declares it.

Parameters:

relations – the structure’s relation symbols.
methods (Dict[str, str]) – {method name: relation symbol}.
equality (str) – the equality symbol, bound to .eq when present.
codec – optional element codec for writing elements as constants.

Return type:

Signature

autstr.symbolic package

Contents

autstr.symbolic package#

Submodules#

autstr.symbolic.backends module#

autstr.symbolic.compiler module#

autstr.symbolic.context module#

autstr.symbolic.expr module#

autstr.symbolic.signature module#

Module contents#