autstr.buildin package

autstr.buildin package#

Submodules#

autstr.buildin.automata module#

autstr.buildin.automata.length_automaton(n, base_alphabet)[source]#

Creates an automaton that recognizes all words over base_alphabet with length exactly n.

Parameters:

  • n (int) – The exact word length

  • base_alphabet (Set[int]) – Set of integer symbols

Return type:

SparseDFA

Returns:

SparseDFA recognizing words of length n

autstr.buildin.automata.k_longer_automaton(k, r, base_alphabet, padding_symbol)[source]#

Creates an automaton recognizing (r+1)-tuples where the last word is at least k letters longer than the other r words.

Parameters:

  • k (int) – Minimal length difference

  • r (int) – Number of reference words

  • base_alphabet (Set[int]) – Set of integer symbols

  • padding_symbol (int) – Padding symbol integer

Return type:

SparseDFA

Returns:

SparseDFA for the k-longer condition

autstr.buildin.automata.zero(symbol_arity=1, base_alphabet=None)[source]#

Automaton that rejects all inputs.

Return type:

SparseDFA

Parameters:

  • symbol_arity (int)

  • base_alphabet (Set[int] | None)

autstr.buildin.automata.one(symbol_arity=1, base_alphabet=None)[source]#

Automaton that accepts all inputs.

Return type:

SparseDFA

Parameters:

  • symbol_arity (int)

  • base_alphabet (Set[int] | None)

autstr.buildin.presentations module#

autstr.buildin.presentations.encode_symbol(tup, base_alphabet)[source]#

Encode a symbol tuple into an integer using base conversion.

Return type:

int

Parameters:
autstr.buildin.presentations.create_sparse_dfa(states, input_symbols, transitions, initial_state, final_states)[source]#

Convert a traditional DFA description to a SparseDFA.

Return type:

SparseDFA

Parameters:
autstr.buildin.presentations.BuechiArithmetic()[source]#

Load the serialized Büchi arithmetic presentation.

Return type:

AutomaticPresentation

autstr.buildin.presentations.buechi_arithmetic()[source]#

Sparse version of Büchi arithmetic over natural numbers. Compiles definable relation from scratch.

Return type:

AutomaticPresentation

autstr.buildin.presentations.BuechiArithmeticZ()[source]#

Load the serialized Büchi arithmetic presentation.

Return type:

AutomaticPresentation

autstr.buildin.presentations.buechi_arithmetic_Z()[source]#

Sparse version of Büchi arithmetic over integers.

Return type:

AutomaticPresentation

autstr.buildin.presentations.MSO0()[source]#

Load the serialized MSO0 presentation.

Return type:

AutomaticPresentation

autstr.buildin.presentations.finite_powerset()[source]#
Return type:

AutomaticPresentation

autstr.buildin.tree_presentations module#

Built-in tree-automatic presentations.

The flagship example is Skolem arithmetic, the multiplicative monoid (N_{>0}, ·): multiplication of naturals is not string-automatic, but the prime-factorization encoding makes it tree-automatic — the multiplicative structure is the direct sum of countably many copies of (N, +), one per prime, and a tree bundles the finitely many nonzero summands.

class autstr.buildin.tree_presentations.SkolemArithmetic(max_states=None)[source]#

Bases: TreeAutomaticPresentation

(N_{>0}, ·, =) presented by tree automata.

Encoding: n = prod_i p_i^{e_i} is a left spine of ‘p’-labelled nodes, one per prime index up to the largest with e_i > 0 (so no trailing zero exponents); spine node i carries e_i as a right-hanging chain of bits with the least significant bit at the top and the most significant (always ‘1’) at the bottom; e_i = 0 is an absent chain. n = 1 is the single node ‘p’.

Relations: M(x, y, z) iff x·y = z, and equality E. Multiplication is positionwise addition of the exponent vectors, so its automaton runs a binary addition automaton independently on every exponent branch of the 3-tape convolution; a single further state rides down the spine and checks that every branch accepted.

Parameters:

max_states (int | None)

LETTERS = frozenset({'*', '0', '1', 'p'})#
PAD = '*'#
classmethod encode(n)[source]#
Return type:

Tree

Parameters:

n (int)

classmethod decode(tree)[source]#
Return type:

int

Parameters:

tree (Tree)

autstr.buildin.tree_presentations.skolem_arithmetic(max_states=None)[source]#
Return type:

SkolemArithmetic

Parameters:

max_states (int | None)

Module contents#