Composing presentations#

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.

autstr.composition performs 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.

Composing presentations

Contents

Composing presentations#

Structures: disjoint union#

Structures: the two direct products#

Classes: union, then all finite products#