AutStr: Symbolic Infinite Structures in Python

AutStr is a Python library for symbolic representation and manipulation of infinite relational structures. It provides automata-based computation, first-order logic queries, and visualization tools for researchers and practitioners in algorithmic model theory.

Key features include:

• Symbolic infinite sets and relations
• Automata-based computation
• First-order logic interface
• Visualization tools

Example algorithms, such as the Sieve of Eratosthenes, demonstrate symbolic computation over infinite sets.

Installation

pip install autstr

Example

Sieve of Eratosthenes (Symbolic Infinite Set)

def infinite_sieve(steps):
    """Sieve of Eratosthenes over infinite integers"""
    candidates = (x.gt(1))  # Initial infinite set: {2,3,4,...}
    primes = []
    for _ in range(steps):
        for p in candidates:
            primes.append(p[0])
            break
        p = primes[-1]
        y = Var("y")
        multiples = (x.eq(p * y)).drop("y")
        candidates = candidates & ~multiples
    return primes, candidates
# Execute first 3 sieving steps
primes, remaining = infinite_sieve(steps=3)
print(f"Primes found: {primes}")
print(f"Remaining infinite set:")
remaining.evaluate().show_diagram()

References

• Abu Zaid, F. Algorithmic Solutions via Model Theoretic Interpretations. Dissertation, RWTH Aachen University, 2016. DOI
• Blumensath, A., & Grädel, E. Automatic Structures. LICS 2000. URL
• Khoussainov, B., & Nerode, A. Automatic presentations of structures. LCC 1994. DOI
• Khoussainov, B., Rubin, S., & Stephan, F. Automatic Structures: Richness and Limitations. LMCS 2007. arXiv DOI