Building new structures from old

Building new structures from old#

Automatic structures over a shared signature are closed under disjoint union and direct products; uniformly automatic classes are closed under union and under taking all finite direct products of their members. They are also closed under first-order interpretation — defining one structure inside another by formulas.

autstr.composition and autstr.interpretations perform these constructions: each takes presentations and returns a presentation, so the result is queried exactly like any other.

Structures: disjoint union#

Two finite linear orders. Their disjoint union has both, and relates nothing across the seam — so it is not itself a linear order.

import numpy as np
from autstr.composition import disjoint_union, direct_product
from autstr.presentations import AutomaticPresentation
from autstr.sparse_automata import SparseDFA
from autstr.utils.misc import encode_symbol


def chain(letters):
    """A finite linear order: one element per letter, ordered as given."""
    alphabet = {'*'} | set(letters)
    code = lambda t: encode_symbol(t, frozenset(alphabet))

    rows = np.full((3, len(letters)), -1, dtype=np.int32)
    to = np.full((3, len(letters)), -1, dtype=np.int32)
    for j, a in enumerate(letters):
        rows[0, j], to[0, j] = code((a,)), 1
    universe = SparseDFA(3, np.array([2, 2, 2], dtype=np.int32), rows, to,
                         [False, True, False], 0, 1, alphabet)

    pairs = [(a, b) for i, a in enumerate(letters) for b in letters[i + 1:]]
    rows = np.full((3, max(len(pairs), 1)), -1, dtype=np.int32)
    to = np.full((3, max(len(pairs), 1)), -1, dtype=np.int32)
    for j, (a, b) in enumerate(pairs):
        rows[0, j], to[0, j] = code((a, b)), 1
    less = SparseDFA(3, np.array([2, 2, 2], dtype=np.int32), rows, to,
                     [False, True, False], 0, 2, alphabet)
    return AutomaticPresentation({'U': universe, 'Lt': less}, padding_symbol='*')


two, one = chain(['p', 'q']), chain(['r'])
both = disjoint_union(two, one)

TOTAL = 'all x.(all y.(Lt(x,y) or Lt(y,x)))'
print("some element is below another:", both.check('exists x.(exists y.(Lt(x,y)))'))
print("the union is a linear order:  ", both.check(TOTAL))

some element is below another: True
the union is a linear order:   False

Structures: the two direct products#

A pair is encoded over the pair alphabet, where a letter carries one letter of each factor. Then

  • sync advances both coordinates: R_A(a,a') ∧ R_B(b,b')

  • async advances exactly one and holds the other: (R_A(a,a') ∧ b=b') ∨ (R_B(b,b') ∧ a=a')

The synchronous product of two strict orders is transitive. The asynchronous one is the grid’s covering relation, and is not — (p,r) < (q,r) < (q,s) while (p,r) and (q,s) are unrelated.

left, right = chain(['p', 'q', 't']), chain(['r', 's', 'u'])
TRANSITIVE = 'all x.(all y.(all z.((Lt(x,y) and Lt(y,z)) -> Lt(x,z))))'

for kind in ('sync', 'async'):
    product = direct_product(left, right, kind=kind)
    print(f"{kind:5s} product of two 3-chains is transitive:",
          product.check(TRANSITIVE))

sync  product of two 3-chains is transitive: True
async product of two 3-chains is transitive: False

Classes: union, then all finite products#

class_union tags the advice, so the two advice languages become disjoint and each member is instantiated by exactly one factor.

direct_product_closure concatenates advices with a separator: the advice α₁ | … | αₙ presents the product of the members that its blocks present. Since an element of a finite member is never longer than its advice, the blocks line up across every tape, and a relation of the product is just the original relation holding in every block — one automaton with one extra state.

from autstr.composition import class_union, direct_product_closure, blocks, tagged_advice
from autstr.groups import ExtraspecialGroups, IndexTwoCyclicGroups
from autstr.uniform import UniformlyAutomaticClass

cyclic, extra = IndexTwoCyclicGroups(), ExtraspecialGroups(3)

def reduct(uniform):                 # the two classes share only U and M
    return UniformlyAutomaticClass(
        {'U': uniform.class_automata['U'], 'M': uniform.class_automata['M']})

both = class_union(reduct(cyclic.cls), reduct(extra.cls))
groups = direct_product_closure(both)
print("alphabet of the product class:", len(groups.base_alphabet), "letters")

alphabet of the product class: 23 letters

z4   = tagged_advice(cyclic.cyclic(4), '<l>')        # Z4, abelian
d4   = tagged_advice(cyclic.advice('dihedral', 4), '<l>')   # D4, nonabelian
heis = tagged_advice(extra.advice(1), '<r>')        # extraspecial 3^(1+2)

ABELIAN  = 'all x.(all y.(all z.(M(x,y,z) -> M(y,x,z))))'
IDENTITY = 'exists u.(all x.(M(x,u,x)))'

members = [("Z4", [z4]), ("Extraspecial(3,1)", [heis]),
           ("Z4 x Z4", [z4, z4]), ("Z4 x Extraspecial(3,1)", [z4, heis]),
           ("D4 x Z4", [d4, z4])]

print(f"{'member':24s} {'identity':>9s} {'abelian':>9s}")
for name, parts in members:
    advice = blocks(*parts)
    print(f"{name:24s} {groups.check(IDENTITY, advice)!s:>9s} "
          f"{groups.check(ABELIAN, advice)!s:>9s}")

member                    identity   abelian
Z4                            True      True
Extraspecial(3,1)             True     False
Z4 x Z4                       True      True
Z4 x Extraspecial(3,1)        True     False
D4 x Z4                       True     False

A product of groups always has an identity, and is abelian exactly when every factor is — one nonabelian factor suffices, and it may come from either family. That last row is what the whole chain of constructions exists to express.

FiniteAbelianGroups in autstr.groups is this same product closure applied to the cyclic groups; it predates the module, which is a good sign the abstraction is the right one.

First-order interpretations#

An interpretation defines a structure inside another one. You give

  • a domain formula \(\delta(\bar x)\) saying which tuples of the source are elements of the new structure — so an element is a \(k\)-tuple, and \(k\) is the interpretation’s dimension;

  • a formula per relation, over \(k\) coordinates per argument;

  • optionally an equivalence \(\varepsilon(\bar x, \bar y)\), and then the elements are its classes.

interpret does not merely record this: it computes the presentation, so the result carries real automata and answers queries at full speed.

The textbook example is the construction of the integers from the naturals. A pair \((a, b)\) stands for \(a - b\), two pairs denote the same integer when \(a + d = c + b\), and the order is \(a + d < c + b\). That is a 2-dimensional quotient interpretation of \((\mathbb{N}, +, <)\) — and here it is.

from autstr.arithmetic import BuechiArithmetic
from autstr.interpretations import interpret

N = BuechiArithmetic()                     # (N, +, <, |2); A(x,y,z) is x + y = z
pair = ['x0', 'x1', 'y0', 'y1']

SAME = 'exists z.(A(x0,y1,z) and A(y0,x1,z))'          # a + d = c + b
LESS = ('exists s.(exists t.(A(x0,y1,s) and A(y0,x1,t) '
        'and Lt(s,t)))')                                # a + d < c + b

Z = interpret(
    N,
    domain=('Eq(x0,x0) and Eq(x1,x1)', ['x0', 'x1']),   # every pair is an element
    relations={'Lt': (LESS, pair), 'Eq': (SAME, pair)},
    dimension=2,
    quotient=(SAME, pair),
)

print('relations:', Z.get_relation_symbols())
print('no least element (unlike N):', Z.check('exists x.(all y.((not Lt(y,x))))'))
print('discrete, not dense:      ',
      not Z.check('all x.(all y.(Lt(x,y) -> exists z.(Lt(x,z) and Lt(z,y))))'))

relations: ['U', 'Lt', 'Eq']
no least element (unlike N): True
discrete, not dense:       True

A codec says what the elements are#

The construction is now correct but illegible: an element of Z is a pair of naturals, and queries hand back the words encoding those pairs. A codec is the missing half — a pair of functions between Python values and the words that represent them. Give one in a Signature, and the structure speaks integers.

Every structure the library ships declares its own this way, which is why symbolic() needs no argument on them. For a structure you build yourself, this is what you write.

from autstr.symbolic import FunctionCodec, Signature

PAD = '*'

def encode(n):
    """n as the pair (a, b) with n = a - b, folded into pair letters."""
    a, b = (n, 0) if n >= 0 else (0, -n)
    wa, wb = N.encode(a), N.encode(b)          # the source structure's own codec
    width = max(len(wa), len(wb))
    return [(wa[i] if i < len(wa) else PAD, wb[i] if i < len(wb) else PAD)
            for i in range(width)]

def decode(word):
    return (N.decode([letter[0] for letter in word])
            - N.decode([letter[1] for letter in word]))

S = Z.symbolic(Signature(codec=FunctionCodec(encode, decode))
               .operator('lt', 'Lt')
               .operator('eq', 'Eq'))
x, y = S.vars('x y')

print('-2 < 3 :', (-2, 3) in x.lt(y))
print(' 3 < -2:', (3, -2) in x.lt(y))
print('solutions of x < 2:', [t for t, _ in zip(iter(x.lt(2)), range(7))])

-2 < 3 : True
 3 < -2: False
solutions of x < 2: [(0,), (-1,), (1,), (-2,), (-3,), (-4,), (-5,)]

The quotient picks one representative per class — over words, the shortlex-least member — so each integer is enumerated once. Over trees no order is well-founded, and the representative is instead the least description of the class (Kuske & Weidner); interpret handles both, since a tree presentation goes in and a tree presentation comes out.

This is how autstr.ordinals is built: the ordinals below \(\omega^n\) are three formulas over Büchi arithmetic — the reverse-lexicographic order on Cantor coefficients — with no automaton authored by hand, and a codec that writes an ordinal as its coefficient tuple.

from autstr.ordinals import Ordinal

w2 = Ordinal(2)                       # the ordinals below omega^2
a, b = w2.symbolic().vars('a b')

# an ordinal is its Cantor coefficients, most significant first:
# (1, 0) is omega, (0, 5) is 5, (1, 1) is omega + 1
print('5 < omega:        ', ((0, 5), (1, 0)) in a.lt(b))
print('omega < 5:        ', ((1, 0), (0, 5)) in a.lt(b))
print('omega+1 < omega*2:', ((1, 1), (2, 0)) in a.lt(b))
print('below omega + 2:  ', [t for t, _ in zip(iter(a.lt((1, 2))), range(5))])

5 < omega:         True
omega < 5:         False
omega+1 < omega*2: True
below omega + 2:   [((0, 0),), ((1, 0),), ((0, 1),), ((1, 1),), ((0, 2),)]

Saving what you built#

Every construction on this page computes automata, and some of them are not cheap. A presentation therefore serializes: automatic_presentation_to_file writes the whole thing — universe, every relation, the alphabet — and automatic_presentation_from_file reads it back.

The payload stores each automaton’s transition diagrams rather than a flat symbol → target table, so a relation over a convolution alphabet too wide to enumerate still writes out in the size of its diagrams.

import tempfile, os
from autstr.presentations import AutomaticPresentation

path = os.path.join(tempfile.mkdtemp(), 'integers.autstr')
Z.automatic_presentation_to_file(path)
print(f'{os.path.getsize(path)} bytes on disk')

reloaded = AutomaticPresentation.automatic_presentation_from_file(path)
print('relations:', reloaded.get_relation_symbols())

# the reloaded structure answers the same questions
R = reloaded.symbolic(Signature(codec=FunctionCodec(encode, decode))
                      .operator('lt', 'Lt').operator('eq', 'Eq'))
a, b = R.vars('a b')
print('-2 < 3 after a round trip:', (-2, 3) in a.lt(b))
print('still discrete:',
      not reloaded.check('all x.(all y.(Lt(x,y) -> exists z.(Lt(x,z) and Lt(z,y))))'))

113559 bytes on disk
relations: ['U', 'Lt', 'Eq']
-2 < 3 after a round trip: True
still discrete: True

What a file does not carry is the signature: a codec is Python code, not data, so a reloaded presentation is a bare structure until you hand it one again. Structures that ship with the library declare their own, which is why BuechiArithmeticZ().symbolic() needs no argument while this one does.

Tree presentations serialize the same way and with the same method names. There the payload matters more, because tree relations are where the expensive constructions live — the reachability relation of a collapsible pushdown graph is exponential in the system’s control states, and once built it is worth keeping.