diff --git a/.claude/settings.json b/.claude/settings.json new file mode 100644 index 0000000..be571f1 --- /dev/null +++ b/.claude/settings.json @@ -0,0 +1,460 @@ +{ + "permissions": { + "allow": [ + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr timeout 1200 /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -c ' *)", + "WebSearch", + "Bash(PYTHONPATH=. timeout 1800 /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -m pytest tests/ -q)", + "Bash(git add *)", + "Bash(git commit -m ' *)", + "Bash(git push *)", + "Bash(awk '{print $2}')", + "Read(//home/faried/.config/pypoetry/**)", + "Bash(poetry config *)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/pip install *)", + "Bash(git tag *)", + "Bash(git checkout *)", + "Bash(git merge *)", + "Bash(poetry publish *)", + "Bash(curl -s https://pypi.org/pypi/autstr/json)", + "Bash(python3 -m venv /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-pypi)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-pypi/bin/pip install *)", + "Bash(ls /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python)", + "Bash(ulimit -v 6000000)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr timeout 600 /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -u /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/probe_3col.py)", + "Bash(mkdir -p /var/home/faried/projects/AutStr/benchmarks)", + "Read(//tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/tasks/**)", + "Bash(grep -v \"^$\")", + "Bash(rm -f abelian_even_order_curve.png pathwidth_curves.png)", + "Bash(rm -rf __pycache__)", + "Bash(systemd-run --user --scope -p MemoryMax=5G -p MemorySwapMax=0 --quiet env PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -u /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/readme_examples.py)", + "Bash(git reset *)", + "Bash(git restore *)", + "Bash(git commit -q -m ' *)", + "Bash(python3 -m venv /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax)", + "Bash(awk '{print $3, $4, $11, $12, $13}')", + "Bash(pkill -f \"pytest /var/home/faried/projects/AutStr/tests/test_tree_automata\")", + "Bash(systemd-run --user --scope -p MemoryMax=4G --quiet env PYTHONPATH=/var/home/faried/projects/AutStr timeout -s ABRT 25 /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -X faulthandler -c ' *)", + "Bash(timeout 20 /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -c ' *)", + "Bash(env PYTHONPATH=/var/home/faried/projects/AutStr timeout 45 /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -m pytest /var/home/faried/projects/AutStr/tests/test_tree_automata.py -x -v)", + "Bash(systemd-run --user --scope -p MemoryMax=4G --quiet env PYTHONPATH=/var/home/faried/projects/AutStr timeout 600 /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -u -c ' *)", + "Bash(awk '{print $3, $4}')", + "Bash(awk '{print $3, $4, $10}')", + "Bash(python3 -)", + "Bash(systemd-run --user --scope -q -p MemoryMax=4G -p MemorySwapMax=0 /tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a-a4d7-45bc-8b9e-c7c87eb6ef00/scratchpad/venv-nojax/bin/python -u -c ' *)", + "Bash(grep -v \"def \\\\|class \\\\|-> \\\\|:.*SparseTreeAutomaton$\")", + "Read(//tmp/claude-1000/-var-home-faried-projects-AutStr/**)", + "Bash(python3 -c \"import numpy, nltk, pytest; print\\('ok'\\)\")", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/200ddc4a*/scratchpad/venv/bin/python -c \"import numpy,nltk,pytest;print\\('venv ok', numpy.__version__\\)\")", + "Bash(./venv/bin/python -c \"import numpy,nltk,pytest;print\\('venv ok',numpy.__version__\\)\")", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_tree_automata.py tests/test_tree_tools.py tests/test_tree_presentations.py tests/test_skolem.py tests/test_tree_uniform.py tests/test_tree_graphs.py tests/test_tree_groups.py -q)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_skolem.py -q)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/pip install *)", + "Bash(cat head.py body.py)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr ./venv/bin/python -c ' *)", + "Bash(PYTHONPATH=. timeout 300 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_tree_automata.py -q)", + "Bash(PYTHONPATH=. timeout 600 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_tree_tools.py -q)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_tree_tools.py --collect-only -q)", + "Bash(PYTHONPATH=. timeout 900 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_tree_presentations.py tests/test_skolem.py -q)", + "Bash(PYTHONPATH=. timeout 900 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_tree_uniform.py tests/test_tree_graphs.py tests/test_tree_groups.py -q)", + "Bash(PYTHONPATH=. timeout 900 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/ -q)", + "Bash(systemd-run --user --scope -q -p MemoryMax=4G -p MemorySwapMax=0 env PYTHONPATH=. AUTSTR_HEAVY=1 timeout 1200 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_tree_graphs.py -q)", + "Bash(sed -i 's/len\\(grp.presentation.base_alphabet\\)/len\\(sta.base_alphabet\\)/' /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/func3.py)", + "Bash(systemd-run --user --scope -q -p MemoryMax=5G -p MemorySwapMax=0 env PYTHONPATH=. timeout 540 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/func3.py)", + "Bash(pkill -f heavy.py)", + "Bash(pkill -f prof.py)", + "Bash(echo \"exit=$?\")", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pyflakes autstr/sparse_automata.py)", + "Bash(PYTHONPATH=. timeout 600 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_arithmetic.py -q)", + "Bash(PYTHONPATH=. timeout 1200 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/ -q)", + "Bash(PYTHONPATH=. timeout 1200 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/ -q --durations=8)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pyflakes autstr/mtbdd.py autstr/sparse_automata.py autstr/sparse_tree_automata.py autstr/utils/automata_tools.py autstr/utils/tree_automata_tools.py)", + "Bash(PYTHONPATH=. timeout 600 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_tree_tools.py tests/test_tree_presentations.py tests/test_tree_uniform.py tests/test_tree_graphs.py -q)", + "Bash(git commit *)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pyflakes autstr/mtbdd.py autstr/sparse_automata.py)", + "Bash(./venv/bin/python -c \"import numpy,nltk,pytest,graphviz,networkx;print\\('venv rebuilt'\\)\")", + "Bash(sed -n '/def _quotient_tree_nfa/,/^ # ---- rebuild/p' autstr/utils/tree_automata_tools.py)", + "Bash(PYTHONPATH=. timeout 600 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/congr.py)", + "Bash(PYTHONPATH=. timeout 900 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/min2.py)", + "Bash(systemd-run --user --scope -q -p MemoryMax=3G -p MemorySwapMax=0 env PYTHONPATH=. timeout 540 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pytest tests/test_clique_width.py -q)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -c ' *)", + "Bash(systemd-run --user --scope -q -p MemoryMax=3G -p MemorySwapMax=0 env PYTHONPATH=.. timeout 540 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python tree_class_benchmark.py --profile light --max-exp 4)", + "Read(//var/home/faried/projects/**)", + "Bash(PYTHONPATH=.. timeout 420 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python uniform_graph_benchmark.py --profile light --max-exp 3)", + "Bash(sed -n '/^## Compiling 3-colourability/,/^## /p' benchmarks/README.md)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -)", + "Bash(PYTHONPATH=.. timeout 900 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/jupyter nbconvert --to notebook --execute --inplace tree_classes.ipynb)", + "Bash(python3 -c ' *)", + "Bash(distrobox list *)", + "Bash(podman ps *)", + "Bash(timeout 300 distrobox enter devbox -- sh -c 'command -v dot || \\(sudo dnf install -y graphviz >/dev/null 2>&1; command -v dot\\)')", + "Bash(timeout 300 distrobox enter devbox -- sh -c 'PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -c \" *)", + "Bash(timeout 1800 distrobox enter devbox -- sh -c 'cd __TRACKED_VAR__/notebooks && for nb in arithmetic mso0 treedepth_graphs; do echo \"--- $nb\"; PYTHONPATH=.. timeout 900 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/jupyter nbconvert --to notebook --execute --inplace $nb.ipynb > /tmp/nbout 2>&1 && echo '\\\\'' ok'\\\\'' || { echo '\\\\'' FAILED'\\\\''; tail -5 /tmp/nbout; }; done')", + "Bash(timeout 600 distrobox enter devbox -- env PYTHONPATH=.. /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/jupyter nbconvert --to notebook --execute --inplace arithmetic.ipynb)", + "Bash(echo \"rc=$?\")", + "Read(//tmp/**)", + "Bash(pkill -9 -f jupyter-nbconvert)", + "Bash(pkill -9 -f ipykernel_launcher)", + "Bash(git status *)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -c 'import autstr; print\\('\\\\''autstr'\\\\'', autstr.__version__\\)')", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pyflakes autstr/mtbdd.py autstr/sparse_automata.py tests/test_closure.py)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pyflakes autstr/closure.py tests/test_closure.py)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pyflakes autstr/closure.py autstr/presentations.py)", + "Bash(git mv *)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -m pyflakes autstr/algebra.py autstr/groups.py autstr/composition.py tests/test_algebra.py tests/test_groups.py tests/test_composition.py)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -c \"import autstr; print\\('version', autstr.__version__\\)\")", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/sphinx-apidoc -f -o docs/source/api autstr)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/sphinx-build -b html docs/source docs/build/html)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/python -c ' *)", + "Bash(env -u PYTHONPATH timeout 1200 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/pytest -q)", + "Bash(git check-ignore *)", + "Bash(git fetch *)", + "Bash(git rev-list *)", + "Bash(git ls-remote *)", + "Bash(env -u PYTHONPATH /tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/venv/bin/twine check dist/*)", + "Bash(grep -E \"LICENSE|pyproject|composition|\\\\.autstr$\")", + "Bash(env)", + "Bash(command -v gh)", + "Bash(gh auth *)", + "Bash(rm -rf /tmp/smoke)", + "Bash(env -u PYTHONPATH bash -e /tmp/smoke_step.sh)", + "WebFetch(domain:docs.github.com)", + "Bash(git ls-tree *)", + "Bash(timeout 200 distrobox enter devbox -- sh -c 'ls ~/.config/gh 2>/dev/null && cat ~/.config/gh/hosts.yml 2>/dev/null | sed \"s/oauth_token:.*/oauth_token: /\"')", + "Bash(python3 -c \"import json,sys; d=json.load\\(sys.stdin\\); print\\(' latest:', d['info']['version'], '| 3.0.0 present:', '3.0.0' in d['releases']\\)\")", + "Bash(timeout 200 distrobox enter devbox -- sh -c 'cd '\\\\''__TRACKED_VAR__'\\\\'' && gh repo view --json nameWithOwner,defaultBranchRef -q '\\\\''.nameWithOwner + \" default=\" + .defaultBranchRef.name'\\\\'' && echo '\\\\''--- existing releases:'\\\\'' && gh release list --limit 5 && echo '\\\\''--- release for v3.0.0?'\\\\'' && \\(gh release view v3.0.0 >/dev/null 2>&1 && echo EXISTS || echo '\\\\''none \\(good\\)'\\\\''\\)')", + "Bash(timeout 300 distrobox enter devbox -- sh -c 'cd '\\\\''__TRACKED_VAR__'\\\\'' && gh release create v3.0.0 --verify-tag --title '\\\\''AutStr 3.0.0 — tree-automatic structures, MTBDD transitions, composition'\\\\'' --notes-file '\\\\''/tmp/claude-1000/-var-home-faried-projects-AutStr/2d526722-67e6-40eb-831e-8c7cfd3aa6ed/scratchpad/RELEASE_NOTES_3.0.0.md'\\\\''')", + "Bash(timeout 200 distrobox enter devbox -- sh -c 'cd '\\\\''__TRACKED_VAR__'\\\\'' && gh run list --workflow=publish.yaml --limit 3')", + "Bash(timeout 200 distrobox enter devbox -- sh -c 'cd '\\\\''__TRACKED_VAR__'\\\\'' && gh run list --limit 6 --json databaseId,name,event,status,conclusion,headBranch --template '\\\\''{{range .}}{{.databaseId}} {{.name}} [{{.event}}] {{.status}} {{.conclusion}}{{\"\\\\n\"}}{{end}}'\\\\''')", + "Bash(timeout 250 distrobox enter devbox -- sh -c 'cd '\\\\''__TRACKED_VAR__'\\\\'' && echo '\\\\''--- runs with event=release:'\\\\'' && gh run list --event release --limit 5 && echo '\\\\''--- workflows known to GitHub:'\\\\'' && gh workflow list --all && echo '\\\\''--- release object:'\\\\'' && gh release view v3.0.0 --json isDraft,isPrerelease,publishedAt,tagName -q '\\\\''.tagName + \" draft=\" + \\(.isDraft|tostring\\) + \" prerelease=\" + \\(.isPrerelease|tostring\\) + \" publishedAt=\" + \\(.publishedAt|tostring\\)'\\\\''')", + "Bash(timeout 250 distrobox enter devbox -- sh -c 'cd '\\\\''__TRACKED_VAR__'\\\\'' && echo '\\\\''--- workflow object:'\\\\'' && gh api repos/fariedabuzaid/AutStr/actions/workflows/310732983 -q '\\\\''.name + \" state=\" + .state + \" path=\" + .path'\\\\'' && echo '\\\\''--- any run at all for it:'\\\\'' && gh api '\\\\''repos/fariedabuzaid/AutStr/actions/workflows/310732983/runs'\\\\'' -q '\\\\''.total_count'\\\\'' && echo '\\\\''--- most recent 3 runs overall \\(any workflow\\):'\\\\'' && gh api '\\\\''repos/fariedabuzaid/AutStr/actions/runs?per_page=3'\\\\'' -q '\\\\''.workflow_runs[] | .name + \" | \" + .event + \" | \" + .conclusion'\\\\''')", + "Bash(python3 -c \"import json,sys; d=json.load\\(sys.stdin\\); print\\(' latest:', d['info']['version'], '| 3.0.0 present:', '3.0.0' in d['releases']\\)\")", + "Bash(awk '/refs\\\\/tags\\\\/v3.0.0\\\\^\\\\{\\\\}/{print \" \" substr\\($1,1,8\\)}')", + "Bash(curl -s https://pypi.org/simple/autstr/)", + "Bash(curl -s -H 'Cache-Control: no-cache' \"https://pypi.org/pypi/autstr/json\")", + "WebFetch(domain:csl2027.github.io)", + "WebFetch(domain:www.fsttcs.org.in)", + "Bash(./venv/bin/python -c \"import numpy, nltk, pytest; print\\('venv ok'\\)\")", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -m pytest tests/test_groups.py -k CutRank -x -q)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/pip install *)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -m pytest -q)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -m pytest tests/test_tree_groups.py -k CutRank -x -q)", + "Bash(echo \"exit: $?\")", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -m sphinx -b html -W --keep-going docs/source /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/docsbuild)", + "Bash(distrobox enter *)", + "Bash(podman pod *)", + "Bash(podman images *)", + "Bash(curl -sfL -o lipics.zip \"https://submission.dagstuhl.de/styles/download-tag/lipics/v2021.1.3/authors/zip\")", + "Bash(unzip -o -q lipics.zip)", + "Bash(curl -sfL -o lipics.tgz \"https://drops.dagstuhl.de/styles/lipics-v2021/lipics-v2021-authors.tgz\")", + "Bash(tar tzf *)", + "Bash(pdfinfo main.pdf)", + "Bash(python3 -m venv /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -m pytest tests/test_cocycle_groups.py -x -q)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -m pytest tests/test_cocycle_groups.py -q --durations=6)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -m pytest tests/test_cocycle_groups.py -q)", + "Bash(podman run *)", + "Bash(pdftotext main.pdf -)", + "Bash(PYTHONPATH=. /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -c ' *)", + "Bash(PYTHONPATH=. timeout 590 /tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad/venv/bin/python -m pytest tests/test_cocycle_groups.py -k Automaton -x -q --durations=3)", + "Bash(ps -eo pid,rss,comm,args --no-headers)", + "Bash(awk '$3 ~ /python/ && $0 ~ /pytest|cocycle/ {print $1, $2, $3}')", + "Bash(SP=/tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad && cat $SP/../tasks/bvtn4phrx.output 2>/dev/null | tail -5; echo ---; tail -4 $SP/heavy_run.log 2>/dev/null)", + "Read(//tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/tasks/**)", + "Bash(systemctl --user list-units --type=scope --no-legend)", + "Bash(SP=/tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad && cat $SP/heavy_run.log; echo \"===\"; cat $SP/../tasks/bvtn4phrx.output 2>/dev/null | tail -3; cat $SP/../tasks/bp55opj0b.output 2>/dev/null | tail -3)", + "Bash(grep -n 'every layout compatible\\\\|total rank of the alternating\\\\|inverses are\\\\|suppressing structural\\\\|row bases of $F_y\\\\|a row of $F_g\\(J\\)$\\\\|hat Q'\\\\''\\\\|co-located\\\\|p + 2$ letters\\\\|prod\\\\\\\\text{-terms\\\\|the run is the word\\\\|dihedral and quaternion\\\\|finitely supported\\\\|right inverse\\\\|n/2 - O\\\\|n/2 -\\\\|width $\\\\\\\\ge n/2' main.tex)", + "Bash(pdftotext -f 1 -l 1 main.pdf -)", + "Bash([ -s $SP/../tasks/b5t7mh2n0.output ])", + "Bash(SP=/tmp/claude-1000/-var-home-faried-projects-AutStr/5da92948-4a90-4ba2-a6be-bb695acdc5d4/scratchpad && cat $SP/../tasks/b5t7mh2n0.output)", + "Bash(pkill -f twosided_search.py)", + "Bash(pdfinfo scratch-chainring.pdf)", + "Bash(pdftotext scratch-chainring.pdf -)", + "Bash(cd /var/home/faried/projects/AutStr/paper && rm -f main.aux main.bbl main.blg main.out main.pdf main.fdb_latexmk main.fls main.log main.vtc && echo \"cleaned\")", + "Bash(grep -viE \"^$\")", + "Bash(timeout 150 poetry run python -c ' *)", + "Bash(timeout 60 poetry run python -c ' *)", + "Bash(poetry run *)", + "Bash(echo \"EXIT=$? DONE\")", + "Bash(grep -nE \"^#{1,4} \" README.md)", + "Bash(sed -n '/\\\\[build-system\\\\]/,/^\\\\[/p' pyproject.toml)", + "Bash(sed -n '/dependencies = \\\\[/,/\\\\]/p' pyproject.toml)", + "Bash(git archive *)", + "Bash(timeout 200 poetry run python benchmarks/implicit_vs_explicit.py --budget-seconds 130 --mem-gb 16 --explicit-timeout 18 --implicit-timeout 15 --max-n-word 3 --max-n-tree 2 --out /tmp/claude-1000/-var-home-faried-projects-AutStr/bf14bf1b-57bf-4218-a192-43611006ec2b/scratchpad/bench_smoke3.md)", + "Bash(git commit -q -m 'Benchmark: sweep width r, center k and depth d; add 4-quantifier query *)", + "Bash(git -C /var/home/faried/projects/AutStr status)", + "Bash(python -m pytest tests/test_groups.py tests/test_tree_groups.py tests/test_cocycle_groups.py -x -q)", + "Bash(ls /var/home/faried/projects/AutStr/.venv/bin 2>/dev/null | head -5; which python3; ls ~/.venvs 2>/dev/null)", + "Read(//home/faried/**)", + "Bash(ls -d /tmp/claude-1000/-var-home-faried-projects-AutStr/*/scratchpad/venv 2>/dev/null | head; ls /tmp/claude-1000/-var-home-faried-projects-AutStr/ 2>/dev/null | head)", + "Bash(python3 -m venv /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/pip -q install nltk pytest numpy)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -c \"import numpy, nltk, pytest; print\\('deps ok'\\)\")", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_groups.py tests/test_tree_groups.py tests/test_cocycle_groups.py -q)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/pip -q install graphviz)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -c \"import ast; ast.parse\\(open\\('autstr/cocycle_groups.py'\\).read\\(\\)\\); print\\('syntax ok'\\)\")", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/bytecompat.py)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_cocycle_groups.py -q)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/ringcheck.py)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -)", + "Bash(ps -eo pid,etime,pcpu,args --no-headers)", + "Bash(awk '$4 ~ /python/ && /scratchpad/ {print $1, $2, $3}')", + "Bash(timeout 280 /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -u -)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/ -q)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/pip -q install networkx)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_groups.py tests/test_implicit.py -q)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_groups.py::TestCutRankGroups::test_validation -q)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_groups.py -q)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_tree_groups.py tests/test_cocycle_groups.py tests/test_implicit.py -q)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_tree_groups.py::TestCutRankTreeGroups::test_width_guard -q)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_tree_groups.py -q)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/ -q -W error::Warning --co -q)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_arithmetic.py -q)", + "Bash(git -C /var/home/faried/projects/AutStr status --short)", + "Bash(git -C /var/home/faried/projects/AutStr diff --stat)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_implicit.py -q)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_rank_width.py -q)", + "Bash(timeout 200 /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -u -)", + "Bash(grep -v \"^\\\\s*$\")", + "Bash(ps -eo pid,etime,pcpu,comm --no-headers)", + "Bash(awk '/sphinx|python3/ && $3 > 50 {print}')", + "Bash(grep -n '`s\\\\b\\\\|`s ' autstr/implicit.py)", + "Bash(git -C /var/home/faried/projects/AutStr remote -v)", + "Bash(git -C /var/home/faried/projects/AutStr branch -a)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -c \"import yaml,sys; d=yaml.safe_load\\(open\\('.github/workflows/run_docs.yaml'\\)\\); print\\('yaml ok — jobs:', list\\(d['jobs']\\)\\); print\\('perms:', d['true'] if 'true' in d else d.get\\('permissions'\\)\\)\")", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/pip -q install pyyaml)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -c ' *)", + "Bash(pdfinfo paper/main.pdf)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -c \"import re; d=open\\('paper/main.log','rb'\\).read\\(\\).decode\\('utf8','ignore'\\); import re; m=re.findall\\(r'Output written on main.pdf \\\\\\(\\(\\\\d+\\) page', d\\); print\\('pages:', m\\)\")", + "Bash(git -C /var/home/faried/projects/AutStr add paper/main.tex)", + "Bash(git -C /var/home/faried/projects/AutStr commit -m ' *)", + "Bash(git -C /var/home/faried/projects/AutStr log --oneline -1)", + "Bash(timeout 500 /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -u -)", + "Bash(timeout 400 /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -u -)", + "Bash(timeout 250 /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -u -)", + "Bash(git -C /var/home/faried/projects/AutStr add paper/main.tex autstr/groups.py tests/test_groups.py FINALIZING.md)", + "Bash(timeout 550 /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -u -)", + "Bash(/tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -u -)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_tree_groups.py tests/test_cocycle_groups.py tests/test_implicit.py tests/test_groups.py -q)", + "Bash(git -C /var/home/faried/projects/AutStr add autstr/tree_groups.py tests/test_tree_groups.py FINALIZING.md)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/ -q -x --ignore=tests/test_cocycle_groups.py)", + "Bash(git -C /var/home/faried/projects/AutStr add autstr/cocycle_groups.py tests/test_cocycle_groups.py paper/main.tex FINALIZING.md)", + "Bash(git -C /var/home/faried/projects/AutStr add README.md)", + "Bash(git -C /var/home/faried/projects/AutStr log --oneline -12)", + "Bash(git -C /var/home/faried/projects/AutStr ls-files paper/)", + "Bash(mkdir -p /var/home/faried/projects/rankwidth-groups-paper)", + "Bash(cp /var/home/faried/projects/AutStr/paper/.gitignore /var/home/faried/projects/AutStr/paper/cc-by.pdf /var/home/faried/projects/AutStr/paper/lipics-logo-bw.pdf /var/home/faried/projects/AutStr/paper/lipics-v2021.cls /var/home/faried/projects/AutStr/paper/main.tex /var/home/faried/projects/AutStr/paper/orcid.pdf /var/home/faried/projects/AutStr/paper/refs.bib /var/home/faried/projects/AutStr/paper/scratch-chainring.tex /var/home/faried/projects/AutStr/paper/theorem3-notes.md /var/home/faried/projects/rankwidth-groups-paper/)", + "Bash(echo \"scratch-chainring.pdf\")", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/a44e92b8-fc14-40a7-8f08-315be4b8cd46/scratchpad/venv/bin/python -m pytest tests/test_groups.py tests/test_chain_ring.py -q)", + "Bash(git -C /var/home/faried/projects/AutStr rm --cached -q .claude/settings.json)", + "Bash(git -C /var/home/faried/projects/AutStr commit --amend --no-edit -q)", + "Bash(git -C /var/home/faried/projects/AutStr show --stat HEAD)", + "Bash(git -C /var/home/faried/projects/AutStr add autstr/cocycle_groups.py)", + "Bash(distrobox enter devbox -- sh -c 'cd ~/projects/AutStr && git add poetry.lock uv.lock pyproject.toml && git commit -q -m \"Rebuild lock files; reconcile sphinx-autodoc-typehints pin *)", + "Bash(python -)", + "Bash(python -c ' *)", + "Bash(python -m pytest tests/test_chain_ring.py tests/test_cocycle_groups.py tests/test_tree_groups.py tests/test_rank_width.py -q)", + "Bash(/var/home/faried/projects/AutStr/.venv/bin/python -m pytest tests/test_chain_ring.py tests/test_cocycle_groups.py tests/test_tree_groups.py tests/test_rank_width.py -q)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_chain_ring.py tests/test_cocycle_groups.py tests/test_tree_groups.py tests/test_rank_width.py tests/test_tree_graphs.py -q)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_chain_ring.py -q)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_tree_groups.py tests/test_rank_width.py -q -x)", + "Bash(git config *)", + "Read(//var/home/faried/**)", + "Bash(flatpak list *)", + "Bash(rpm -q code)", + "Bash(git -C /var/home/faried/projects/AutStr branch --show-current)", + "Bash(timeout 300 .venv/bin/python -c ' *)", + "Bash(python3 -c \"import numpy\")", + "Read(//var/home/faried/.cache/pypoetry/virtualenvs/**)", + "Bash(timeout 600 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -c ' *)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -c ' *)", + "Bash(timeout 120 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -c ' *)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/b85bf2ed-1f4c-4f2e-8358-3348f99e2d8d/scratchpad/t1.py)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -u /tmp/claude-1000/-var-home-faried-projects-AutStr/b85bf2ed-1f4c-4f2e-8358-3348f99e2d8d/scratchpad/t1.py)", + "Bash(timeout 1800 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_symbolic.py -q)", + "Bash(timeout 600 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -u -c ' *)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -u -c ' *)", + "Bash(timeout 1800 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_arithmetic.py tests/test_symbolic.py -q)", + "Bash(timeout 3000 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/ -q -x --timeout=600)", + "Bash(timeout 3000 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/ -q)", + "Bash(timeout 60 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -c ' *)", + "Bash(timeout 60 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_symbolic.py -q)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_symbolic.py tests/test_arithmetic.py -q)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python scripts/gen_readme_media.py)", + "Bash(awk '{print \"still running, cpu-time:\", $10}')", + "Bash(awk '{print \"cpu-time:\", $10}')", + "Bash(timeout 300 uv sync --dry-run)", + "Bash(timeout 900 uv sync)", + "Bash(timeout 900 uv sync --python 3.13)", + "Bash(.venv/bin/python -c ' *)", + "Bash(timeout 900 .venv/bin/python -m pytest tests/test_symbolic.py tests/test_arithmetic.py -q)", + "Bash(.venv/bin/python -c \"import jax\")", + "Bash(command -v dot)", + "Bash(rm -rf /tmp/uvcheck)", + "Bash(.venv/bin/python -c \"import sys,numpy,nltk;print\\('python',sys.version.split\\(\\)[0],'| numpy',numpy.__version__\\)\")", + "Bash(timeout 60 .venv/bin/python -c ' *)", + "Bash(timeout 900 .venv/bin/python -u -c ' *)", + "Bash(chmod +x drive.sh)", + "Bash(./drive.sh)", + "Bash(tee sweep.csv)", + "Bash(python3 -c \"import autstr\")", + "Bash(chmod +x drive_b.sh)", + "Bash(./drive_b.sh)", + "Bash(tee sweep_b.csv)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 180 env PYTHONPATH=/var/home/faried/projects/AutStr /var/home/faried/projects/AutStr/.venv/bin/python3 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/verify_instance.py)", + "Bash(python3 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/edit_nb.py)", + "Bash(.venv/bin/python3 -m pytest --version)", + "Bash(.venv/bin/python3 -c \"import pytest_timeout; print\\('pytest-timeout available'\\)\")", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 2400 .venv/bin/python3 -m pytest tests/ -v --durations=20 -p no:cacheprovider)", + "Bash(echo \"EXIT=$?\")", + "Bash(.venv/bin/python3 -c \"import nbstripout; print\\('installed'\\)\")", + "Bash(timeout 180 .venv/bin/python3 -m pre_commit run --all-files)", + "Read(//var/home/linuxbrew/.linuxbrew/Cellar/git-lfs/3.7.1/bin/**)", + "Read(//home/faried/.linuxbrew/bin/**)", + "Bash(git-lfs version *)", + "Bash(git lfs *)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 600 .venv/bin/python3 -m pytest tests/test_symbolic_tree.py -x -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_symbolic_tree.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 2400 .venv/bin/python3 -m pytest tests/ -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_tree_automata.py -q -p no:cacheprovider)", + "Bash(.venv/bin/python3 -c ' *)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=2G -- timeout 300 .venv/bin/python3 -m pytest tests/test_symbolic_tree.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=2G -- timeout 300 .venv/bin/python3 -m pytest tests/test_symbolic_tree.py tests/test_tree_automata.py -q -p no:cacheprovider)", + "Bash(sed -i 's/ The tree engine has no counterpart yet for enumeration, which raises with\\\\n the reason rather than quietly answering a different question./X/' autstr/symbolic/backends.py)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 600 .venv/bin/python3 -c ' *)", + "Bash(sed -i '52s/.*/from autstr.sparse_tree_automata import SparseTreeAutomaton, Tree/' autstr/utils/tree_automata_tools.py)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 300 .venv/bin/python3 -c ' *)", + "Bash(sed -i 's/^from autstr.sparse_tree_automata import \\(/from autstr.utils.tree_automata_tools import _shortlex_key, iterate_trees\\\\nfrom autstr.sparse_tree_automata import \\(/' tests/test_tree_automata.py)", + "Bash(sed -i 's/ for letter in sorted\\(alphabet\\) if letter != padding_symbol/ for letter in sorted\\(alphabet\\)/' autstr/utils/tree_automata_tools.py)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 600 .venv/bin/python3 -m pytest tests/test_symbolic_tree.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=2G -- timeout 300 .venv/bin/python3 -m pytest tests/test_tree_tools.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_tree_uniform.py -q -p no:cacheprovider)", + "Bash(sed -i 's/^from autstr.sparse_tree_automata import SparseTreeAutomaton, Tree$/from autstr.sparse_tree_automata import SparseTreeAutomaton, Tree\\\\nfrom autstr.symbolic import FunctionCodec, Signature/' tests/test_tree_uniform.py)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -c ' *)", + "Bash(.venv/bin/python3 -c \"from autstr.symbolic import operation_signature, EQUALITY_SYMBOLS; print\\('exports ok', EQUALITY_SYMBOLS\\)\")", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_symbolic.py tests/test_symbolic_tree.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 1500 .venv/bin/python3 -c ' *)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -- timeout 600 .venv/bin/python3 -c ' *)", + "Bash(.venv/bin/python3 -c \"from autstr.symbolic import operation_signature, EQUALITY_SYMBOL; print\\('ok', EQUALITY_SYMBOL\\)\")", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -- timeout 900 .venv/bin/python3 -c ' *)", + "Bash(.venv/bin/python3 -c \"import autstr.tree_graphs, autstr.graphs, autstr.algebra; print\\('modules import ok'\\)\")", + "Bash(.venv/bin/python3 -c \"import autstr.tree_graphs, autstr.graphs, autstr.algebra, autstr.groups; print\\('modules import ok'\\)\")", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_equality.py -q -p no:cacheprovider)", + "Bash(.venv/bin/python3 -c \"import sphinx, myst_nb; print\\('sphinx', sphinx.__version__\\)\")", + "Bash(.venv/bin/python3 -c \"import sphinx; print\\('sphinx', sphinx.__version__\\)\")", + "Bash(.venv/bin/python3 -)", + "Bash(which uv *)", + "Read(//home/linuxbrew/.linuxbrew/bin/**)", + "Bash(uv venv *)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 env PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/docsvenv/bin/python -m sphinx.ext.apidoc -f -o /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/apidoc autstr)", + "Bash(echo \"apidoc EXIT=$?\")", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 1200 env PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/docsvenv/bin/python -m sphinx -b html --keep-going -D nb_execution_mode=off docs/source /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/docsbuild)", + "Bash(PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/docsvenv/bin/python -c 'import autstr.algebra')", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -- timeout 900 env PYTHONPATH=/var/home/faried/projects/AutStr /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/docsvenv/bin/python -m sphinx -b html --keep-going -D nb_execution_mode=off docs/source /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/docsbuild3)", + "Bash(grep WARNING __TRACKED_VAR__/docsbuild3.log)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_infinite_extraspecial.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -- timeout 600 .venv/bin/python3 -m pytest tests/test_infinite_extraspecial.py -q -p no:cacheprovider)", + "WebFetch(domain:arxiv.org)", + "WebFetch(domain:www.irif.fr)", + "WebFetch(domain:d-nb.info)", + "Bash(pdftotext webfetch-1786476185248-qqkzxh.pdf -)", + "Bash(pdftotext webfetch-1786476190531-ui46ls.pdf -)", + "Bash(git switch *)", + "Bash(git pull *)", + "Bash(.venv/bin/python3 -c \"from autstr.symbolic import graph_signature; print\\('exported:', graph_signature.__name__\\)\")", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 600 .venv/bin/python3 -m pytest tests/test_infinite_graphs.py -q -p no:cacheprovider)", + "Bash(.venv/bin/python3 -c \"from autstr.arithmetic import encode, decode; print\\('codec fns ok:', encode\\(7\\), decode\\(encode\\(7\\)\\)\\)\")", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_integer_grid.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 600 .venv/bin/python3 -m pytest tests/test_integer_grid.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_interpretations.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -- timeout 500 .venv/bin/python3 -c ' *)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -- timeout 400 .venv/bin/python3 -c ' *)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 900 .venv/bin/python3 -m pytest tests/test_interpretations.py tests/test_automata_tools.py -q -p no:cacheprovider)", + "Bash(kill %1)", + "Bash(pkill -f \"pytest tests/test_interpretations\")", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 400 .venv/bin/python3 -m pytest tests/test_interpretations.py tests/test_automata_tools.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -- timeout 300 .venv/bin/python3 -c ' *)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -p MemorySwapMax=0 -- timeout 600 .venv/bin/python3 -m pytest tests/test_interpretations.py tests/test_automata_tools.py tests/test_integer_grid.py -q -p no:cacheprovider)", + "Bash(systemd-run --user --scope --quiet -p MemoryMax=3G -- timeout 300 .venv/bin/python3 /tmp/claude-1000/-var-home-faried-projects-AutStr/2d9a6131-5471-4026-977d-846f68bb33e8/scratchpad/fold_diag_repro.py)", + "Bash(ls /tmp/claude-1000/-var-home-faried-projects-AutStr/*/scratchpad/ 2>/dev/null)", + "Bash(python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/batch_repro.py)", + "Read(//var/home/faried/.local/share/uv/python/cpython-3.13.14-linux-x86_64-gnu/bin/**)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/batch_repro.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/kdim_repro.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/kdim_quot.py)", + "Bash(sed -i 's/from autstr.buildin.presentations import BuechiArithmeticN, BuechiArithmeticZ/from autstr.buildin.presentations import BuechiArithmetic/; s/^SRC = SRC$/SRC = BuechiArithmetic/' /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/kdim_quot.py)", + "Bash(sed -i 's/^SRC = BuechiArithmeticN$/SRC = BuechiArithmetic/' /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/kdim_quot.py)", + "Bash(.venv/bin/python -m pytest tests/ -q -p no:randomly)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/scan.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/scan2.py 2418 2456)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/scan2.py 2380 2418)", + "Bash(.venv/bin/python -)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/scan2.py 2316 2362)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/diag_bug.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/diag_bug2.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/witness.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/witness2.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/src_level.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/universe.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/kdim_fresh.py)", + "Bash(.venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/compare.py)", + "Bash(.venv/bin/python scripts/gen_builtin_presentations.py)", + "Bash(timeout 600 .venv/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/cbe3da38-e60d-426a-b319-7761c21ba7e9/scratchpad/quot2.py)", + "Bash(timeout 900 .venv/bin/python -m pytest tests/test_presentations.py tests/test_interpretations.py -q -p no:cacheprovider)", + "Bash(timeout 2400 .venv/bin/python -m pytest tests/ -q -p no:cacheprovider)", + "Read(//home/faried/.claude/**)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/ -q -x --timeout=600)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/ -q)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -c ' *)", + "Bash(time ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -c ' *)", + "Bash(time ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_ordinals.py -q)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_ordinals.py -q)", + "Bash(timeout 300 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_regular_tree.py -q)", + "Bash(timeout 600 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_presentations.py -q)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -)", + "Bash(timeout 300 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -c ' *)", + "Bash(timeout 600 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_turing.py -q)", + "Bash(timeout 300 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_regular_tree.py tests/test_integer_grid.py tests/test_infinite_graphs.py -q)", + "Bash(ps -eo pid,stat,etime,time,%cpu,%mem,rss,comm --sort=-%mem)", + "Bash(timeout 600 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_automata_tools.py -q)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python /tmp/claude-1000/-var-home-faried-projects-AutStr/8ea117be-ee5c-4752-bcca-214821a7c09a/scratchpad/probe_sentences.py)", + "Bash(~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pyflakes autstr/interpretations.py)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_tree_tools.py -q)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_tree_interpretations.py -q)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_tree_interpretations.py tests/test_interpretations.py tests/test_tree_presentations.py tests/test_symbolic_tree.py -q)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_tree_presentations.py -q)", + "WebFetch(domain:eiche.theoinf.tu-ilmenau.de)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_tree_interpretations.py tests/test_interpretations.py -q)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_ordinals.py -q)", + "Bash(timeout 900 ~/.cache/pypoetry/virtualenvs/autstr-Ff0G8Q62-py3.13/bin/python -m pytest tests/test_tree_algebra.py -q)", + "Bash(git branch *)", + "Bash(gh pr *)", + "WebFetch(domain:ar5iv.labs.arxiv.org)", + "Bash(curl -sL -o k.tar.gz \"https://arxiv.org/e-print/1303.2453\")", + "Bash(mkdir -p kartzow)", + "Bash(tar xzf *)", + "Bash(git rebase *)", + "Bash(ps -eo pid,etime,args --no-headers)", + "Bash(awk '$3 ~ /pytest|python/ && $0 !~ /awk/')", + "Bash(pdftotext -layout kw.pdf kw.txt)", + "Bash(git cherry-pick *)", + "Bash(awk -F: '$1 > 1600 && $1 < 2400')", + "Bash(curl -sL -o thesis.tar.gz \"https://arxiv.org/e-print/1202.0137\")", + "Bash(mkdir -p thesis)", + "Bash(awk -F: '$1 > 639 && $1 < 2396')", + "Bash(timeout 300 distrobox enter devbox -- bash -lc 'PYTHONPATH=. .venv/bin/python -u /tmp/claude-1000/-var-home-faried-projects-AutStr/f653607e-ac8b-43c1-8960-acd739422fab/scratchpad/summary_check.py')", + "Bash(timeout 900 distrobox enter devbox -- bash -lc 'PYTHONPATH=. .venv/bin/python -u /tmp/claude-1000/-var-home-faried-projects-AutStr/f653607e-ac8b-43c1-8960-acd739422fab/scratchpad/random_check.py')", + "Bash(sed -i 's/for trial in range\\(60\\):/for trial in range\\(200\\):/; s/60 systems/200 systems/' random_check.py)", + "Bash(timeout 1800 distrobox enter devbox -- bash -lc 'PYTHONPATH=. .venv/bin/python -u /tmp/claude-1000/-var-home-faried-projects-AutStr/f653607e-ac8b-43c1-8960-acd739422fab/scratchpad/random_check2.py')", + "Bash(awk '{print} /missing/ && !/0 missing, 0 extra/ {bad++} END {print \"systems with disagreements:\", bad+0}')", + "Bash(timeout 2400 distrobox enter devbox -- bash -lc 'PYTHONPATH=. .venv/bin/python -u /tmp/claude-1000/-var-home-faried-projects-AutStr/f653607e-ac8b-43c1-8960-acd739422fab/scratchpad/d_check.py')" + ], + "additionalDirectories": [ + "/var/home/faried/projects/AutStr", + "/var/home/faried/projects/AutStr/paper", + "/dev", + "/var/home/faried/projects/rankwidth-groups-paper" + ] + } +} diff --git a/.github/workflows/publish.yaml b/.github/workflows/publish.yaml index 40e5592..3e59519 100644 --- a/.github/workflows/publish.yaml +++ b/.github/workflows/publish.yaml @@ -63,7 +63,7 @@ jobs: /tmp/smoke/bin/pip install --quiet dist/*.whl /tmp/smoke/bin/python -c " import autstr - from autstr.buildin.presentations import BuechiArithmeticZ + from autstr.arithmetic import BuechiArithmeticZ assert BuechiArithmeticZ().check('exists x.(A(x,x,x))') print('smoke test passed for', autstr.__version__) " diff --git a/.gitignore b/.gitignore index 89c79c8..bcc1ca9 100644 --- a/.gitignore +++ b/.gitignore @@ -141,3 +141,4 @@ docs/source/api/ docs/source/notebooks/ docs/source/jupyter_execute/ docs/source/_media/ +docs/source/changelog.md diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..53d7793 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,279 @@ +# Changelog + +All notable changes to AutStr are recorded here. Versions follow +[semantic versioning](https://semver.org): the major number changes when +existing code has to be edited to keep working. + +Each release since v2.0 is also a snapshot of an experiment in AI-assisted +algorithm engineering — see the [README](https://github.com/fariedabuzaid/AutStr#readme) for that story. + +--- + +## v4.0.0 — August 2026 + +**The symbolic release.** Queries stop being strings, structures start +declaring their own vocabulary, and the package stops pretending some of its +structures are more "built in" than others. + +### Added + +**A generic first-order layer — `autstr.symbolic`.** +Variables, relation symbols and function symbols that compose with ordinary +Python operators, compiled against either engine and against uniformly +automatic classes: + +```python +x, y, z = BuechiArithmeticZ().symbolic().vars('x y z') +phi = (x + y).eq(z) & z.lt(100) +phi.check() # satisfiable? +(3, 4, 7) in phi # membership +list(phi.drop(z)) # enumerate, smallest first +``` + +- `Signature` declares which relations are function graphs, which Python + operator each binds to, and — via an `ElementCodec` — how Python values + encode as elements. Terms nest (`((x + y) + z).eq(10)`), arities come from + the automata, and variable names survive into results. +- Quantifiers (`.all`, `.drop`, `.exinf`), Boolean connectives, `is_finite`, + membership, and lazy enumeration in length-lexicographic order. +- The same expressions compile against a class, where `check_member` and + `evaluate_member` decide one member — explicitly or implicitly. +- Ready-made signature builders: `operation_signature`, `order_signature`, + `graph_signature`, `relational_signature`. + +**Every structure declares its own vocabulary.** +`symbolic()` now takes no argument on every structure the library ships: +each provides `default_signature`, so operators and a codec are there from the +start. Büchi arithmetic over ℕ and over ℤ and the MSO0 powerset structure +gained theirs in this release; MSO0's is new capability rather than +convenience — union, intersection and difference as `+`, `*`, `-`, with +solutions returned as Python sets. + +**First-order interpretations — `autstr.interpretations`.** +`interpret` *computes* the interpreted presentation from a domain formula, a +formula per relation, an optional dimension *k* (elements are *k*-tuples) and +an optional definable equivalence: + +- quotients over words take the shortlex-least member of a class as its + representative; +- quotients over **trees** take the least *description*, since no order on + trees is well-founded (Kuske & Weidner) — the same idea made to work without + a well-order; +- `representatives` exposes the chosen representative of each class. + +**Infinite graphs — `autstr.infinite_graphs`, `autstr.turing`.** +`InfiniteGraph` is the shared surface (edge relation, symmetry check, codec); +concrete members are `IntegerGrid` (the Cayley graph of ℤⁿ, built as an +asynchronous product), `RegularTree` (T_k with successors and the prefix +order), and `ConfigurationGraph` for a Turing machine — whose first-order +theory is decidable while reachability, being halting, is not. + +**Ordinals — `autstr.ordinals`.** The ordinals below ω^ω on the string engine +and below ω^(ω^n) on the tree engine, each *interpreted* in arithmetic rather +than authored: three formulas over Büchi arithmetic, with the +reverse-lexicographic order on Cantor coefficients. + +**The countable atomless Boolean algebra — `autstr.tree_algebra`.** The clopen +algebra of Cantor space, with meet, join and complement as terms, and +`is_atomless` as a decided sentence rather than an assertion. + +**Level 2 collapsible pushdown graphs — `autstr.collapsible`.** +Stacks of stacks with collapse links, presented by Kartzow's tree encoding: +blocks hang off each other as right children, links are recovered from the +tree's shape rather than stored, and every stack operation is a bounded rewrite +at the end of the last path. MSO over these graphs is undecidable, so the tree +encoding is the only automatic route to them. + +**Reachability for those graphs — `autstr.collapsible_reach`.** +`Reach` is a relation of the configuration graph, so a first-order formula may +ask about runs of *any* length — the question a Turing machine's configuration +graph cannot answer. Following Kartzow's decomposition, every run splits into +four stretches and reachability is the first-order formula + + Reach(x,y) = ∃d ∃f ∃g. A(x,d) ∧ B(d,f) ∧ C(f,g) ∧ D(g,y) + +over four reflexive relations — no fifth automaton and no fixpoint over trees. +Underneath, `Summaries` computes per-word returns and loops by saturation +(the paper's own effectiveness argument routes through µ-calculus model +checking, which is not needed), and the nondeterministic guesses of Kartzow's +automata are carried on annotation tapes that are projected away — the move +MONA makes. `reach_along` builds the label-constrained `Reach_L` by putting +the label automaton into a product system; ε-contraction is a special case. + +**Serialization for the tree engine.** `SparseTreeAutomatonSerializer` and +`TreeAutomaticPresentationSerializer`, with the same method names as the string +side (`automatic_presentation_to_file` / `..._from_file`). A tree automaton's +compiled form is a sorted table of child pairs with one decision-diagram root +each, so the payload is the pair keys plus the shared sub-DAG below those +roots — a relation over an alphabet too wide to enumerate still writes out in +the size of its diagrams. This is where it earns its keep: `Reach` is +exponential in the control states, and a reloaded copy is still reachability. + +**Deferred relations.** A presentation may declare a relation now and build it +on first use. `get_relation_symbols()` lists it, a query that mentions it +triggers the build. This is how `Reach` avoids costing anything until asked +for, and it is the opt-out for every expensive relation. + +**Smaller additions.** `partial_dfa` / `partial_tree_automaton`; +`restrict_alphabet`; `fold_tapes` for tree automata; `tree_order` and +`domain_within`; sentences usable as operands of a connective; an `Eq` +relation on every presentation. + +### Changed + +- **`autstr.buildin` is gone.** Every structure the library ships is built in, + so the name carved nothing. Its contents moved to where their subject lives: + + | was | now | + |---|---| + | `autstr.buildin.presentations` | `autstr.arithmetic` (Büchi ℕ and ℤ) and `autstr.powerset` (MSO0) | + | `autstr.buildin.tree_presentations` | `autstr.tree_arithmetic` (Skolem arithmetic) | + | `autstr.buildin.automata` | `autstr.utils.automata_tools` | + +- **`autstr.arithmetic` is a different module.** It holds the two Büchi + presentations themselves; the old term-algebra front end + (`VariableETerm` and friends) is replaced by the symbolic layer. +- `encode` / `decode` are now static methods on the presentations that own + them. +- Documentation builds execute every notebook, and the repository keeps them + output-free. + +### Fixed + +- **Enumeration over a product alphabet.** Every interpreted structure of + dimension > 1 — including the shipped `Ordinal(2)` — produced unusable + results from `iter(...)`: tapes were built by string-concatenating letters, + which holds only while a letter is a single character, so a tuple letter was + flattened into text no codec could read. Membership was unaffected, which is + why it went unseen. +- **Serializing such a presentation.** JSON has no tuples, so a reloaded + product alphabet was a set of lists (unhashable) and the padding symbol a + list. Both are restored on load, on both engines. +- A universal quantifier that silently became an existential. +- Sentence markers that dropped the structure's alphabet. +- Relation automata are restricted to the universe on *every* tape, not all but + the last: a relation that still held of a non-element made universal + sentences false on encodings that were not elements at all. +- Spliced relations are restored even when a query fails. + +### Removed + +- **The precompiled `.autstr` artifacts.** They saved 0.03 s, 0.23 s and + 0.44 s against building from scratch, and the built presentations are + identical to the loaded ones relation by relation. Serialization itself is + unchanged and fully supported — see the composition notebook. +- `scripts/gen_builtin_presentations.py`, which generated them. + +### Upgrading from 3.x + +```python +# 3.x +from autstr.buildin.presentations import BuechiArithmeticZ, MSO0 +from autstr.buildin.tree_presentations import skolem_arithmetic +from autstr.arithmetic import integers, encode, decode + +# 4.0 +from autstr.arithmetic import BuechiArithmeticZ # .encode / .decode on it +from autstr.powerset import MSO0 +from autstr.tree_arithmetic import skolem_arithmetic +Z = BuechiArithmeticZ().symbolic() # was integers() +``` + +--- + +## v3.1.0 — July 2026 + +The rank-width release: new mathematics on top of the v3 engines. + +### Added + +- **Class-2 groups of bounded rank-width.** `CutRankGroups` (linear layouts), + `CutRankTreeGroups` (tree layouts) and `CocycleRankWidthGroups` (distributed + centers, microcode advice) — the advice spells out rank-≤r factorizations of + the commutation form's crossing blocks, cut by cut. +- **The chain-ring extension** (`autstr.chain_ring`). Everything generalizes + from F_p to R = ℤ/pᵈ: Smith normal form, saturated interfaces, the two-sided + factorization lemma. Centers of exponent pᵈ, widths measured as module + cut-rank, byte-identical at d = 1. +- **Factored advice letters.** Beyond ~20000 flat letters the cut-rank classes + stream one ring entry per letter through accumulator states, making width + r ≥ 2 over the ring representable (q+1 advice letters). +- **Implicit evaluation** (`autstr.implicit`). `check_implicit` / + `evaluate_implicit` on every class: first-order model checking and + satisfying-set computation that never build a query — or even a base — + automaton, reaching members (ℤ/8 and ℤ/9 words, ℤ/4 trees, the + distributed-center protocol) whose automata are infeasible. `ImplicitClass` / + `ImplicitTreeClass` are presentations given purely by transition functions. +- **Graphs of bounded rank-width.** `RankWidthClass` — rank decompositions as + advice, adjacency as a bilinear form on r-bit interface vectors, full MSO. + +### Changed + +- `show_diagram` no longer opens an external image viewer by default; pass + `view=True` for the old behavior. + +--- + +## v3.0.0 — July 2026 + +From strings to trees, with the transition representation replaced underneath +both engines. + +### Added + +- **Tree-automatic structures.** `autstr.sparse_tree_automata` (bottom-up tree + automata), `autstr.tree_presentations` and `autstr.tree_uniform` — the tree + counterparts of the whole stack. New members: **Skolem arithmetic** (ℕ, ·), + graphs of bounded **tree-width** and **clique-width** with full MSO, and + tree-indexed **extraspecial p-groups**. Cross-validated by embedding the + string engine's Büchi arithmetic into the tree engine and re-deciding every + sentence through both. +- **Composing presentations** (`autstr.composition`): disjoint union, + synchronous and asynchronous direct products of automatic structures, union + of uniformly automatic classes, and the direct-product closure of a class. + Composed, they present every finite direct product of index-≤2 cyclic groups + and extraspecial p-groups, from either family, and decide that such a product + is abelian exactly when all of its factors are. + +### Changed + +- **Transitions are shared multi-terminal BDDs** over the symbol's digits, in + both engines (`autstr.mtbdd`). `expand` became a variable renaming, + `complement` stopped touching diagrams at all, and `minimize` became one + `apply` per state per round. Queries impossible for lack of alphabet width + now compile: an arity-5 relation over a 14-letter alphabet (14⁵ = 537 824 + flat symbols) went from *infeasible* to 0.2 s; tree-depth-4 bipartiteness + from 17 s to 0.4 s. The test suite went from ~2 min to ~35 s. + +--- + +## v2.0.0 — July 2026 + +### Added + +- The whole uniformly-automatic layer: the generic advice machinery, bounded + tree-depth and pathwidth graphs with MSO, finite Boolean algebras, finite + abelian groups, the ℤ[1/p] presentations, and the non-abelian group classes — + each verified against exhaustive or exact ground-truth oracles. +- The [benchmark suite](https://github.com/fariedabuzaid/AutStr/tree/main/benchmarks) and the documentation site. + +### Changed + +- The automata core was profiled and rewritten as batched, sparsity-aware + NumPy: a **10²–10³× speedup** (the reference query dropped from 85 s to + 0.03 s), with linear memory. +- JAX went from a hard dependency to an optional accelerator; NumPy is the + canonical core. + +--- + +## v1.x — July 2025 + +Added the sparse-DFA backend, serialization, and the MSO0 finite-powerset +structure; modernized packaging. + +--- + +## v1.0 — 2022 + +The original library and its arithmetic front end. diff --git a/README.md b/README.md index cfeb484..75fd0b0 100644 --- a/README.md +++ b/README.md @@ -43,27 +43,39 @@ from different angles. pip install autstr ``` -The friendliest entry point is the arithmetic package: relations over the -integers are first-class, exactly-represented **infinite** objects that you -combine with relational algebra. +Ask any structure for its **symbolic interface** and it hands you variables that +compose with ordinary Python operators. Relations are first-class, +exactly-represented **infinite** objects. ```python -from autstr.arithmetic import VariableETerm as Var +from autstr.arithmetic import BuechiArithmeticZ -x, y, z = Var('x'), Var('y'), Var('z') +Z = BuechiArithmeticZ().symbolic() # (ℤ, +, <, |₂); no setup required +x, y, z = Z.vars('x y z') R = (x + y + 3).lt(2 * x) # the infinite set { (x, y) : x + y + 3 < 2x } -R.isempty() # False +R.is_empty() # False (0, 4) in R # False — membership test band = (x + y).eq(z) & z.gt(0) & z.lt(3) # x + y = z ∧ 0 < z < 3 -solutions = band.drop(['z']) # project z away (an ∃ quantifier) -for s, _ in zip(solutions, range(3)): # enumerate lazily, smallest-first - print(s) # (0, 1), (1, 0), (1, 1), ... +for s, _ in zip(band.drop(z), range(3)): # ∃z, then enumerate smallest-first + print(s) # (0, 1), (1, 0), (1, 1) ``` Nothing is materialized until you iterate; `& | ~` are exact operations on -infinite sets. +infinite sets. Integers go in and come out because the structure ships a +**codec** along with its operators — and so does every other structure here, so +the same expressions work elsewhere unchanged: + +```python +from autstr.powerset import MSO0 + +a, b, c = MSO0().symbolic().vars('a b c') # finite sets of naturals +({0, 1}, {1, 2}, {0, 1, 2}) in (a + b).eq(c) # union — True +``` + +Where a formula reads better as text, `check` and `evaluate` still take +strings; the two are interchangeable. --- @@ -82,7 +94,7 @@ fragment these structures capture — and `evaluate` returns the automaton of *a satisfying assignments, which you can enumerate or reuse. ```python -from autstr.buildin.presentations import BuechiArithmeticZ +from autstr.arithmetic import BuechiArithmeticZ Z = BuechiArithmeticZ() # (ℤ, +, <, |) as automata Z.check('all x.(exists y.(A(x,y,x)))') # ∀x ∃y: x+y=x — True @@ -129,7 +141,7 @@ batch: | package | structures | |---------|------------| -| `autstr.arithmetic`, `autstr.buildin` | Presburger and Büchi arithmetic (ℤ, +, <, \|₂), Skolem arithmetic (ℕ, ·), the MSO0 finite-powerset structure | +| `autstr.arithmetic`, `autstr.tree_arithmetic`, `autstr.powerset` | Presburger and Büchi arithmetic (ℤ and ℕ, +, <, \|₂), Skolem arithmetic (ℕ, ·) on the tree engine, the MSO0 finite-powerset structure | | `autstr.algebra`, `autstr.tree_algebra` | the localizations **ℤ[1/p]**, finite **Boolean algebras**, and the countable **atomless Boolean algebra** | | `autstr.infinite_graphs`, `autstr.ordinals`, `autstr.turing` | the **integer grid** ℤⁿ, the **regular tree** T_k, the **ordinals** below ω^ω and — on the tree engine — below ω^(ω^ω), **Turing-machine configuration graphs** | | `autstr.collapsible`, `autstr.collapsible_reach` | **level 2 collapsible pushdown graphs** — tree-automatic by Kartzow's encoding, and the one automatic route to them, since their MSO theory is undecidable. **Reachability** is a relation of the graph, so first-order formulas may ask about runs of any length — the question a Turing machine's configuration graph cannot answer | @@ -162,8 +174,8 @@ Four capabilities cut across all of these: Büchi's theorem to Rabin's. The executable notebooks in [`notebooks/`](notebooks/) work through all of it, -one per area — arithmetic & algebra, graphs, groups, composition, and implicit -evaluation. +one per area — arithmetic & algebra, infinite structures, graphs, groups, +composition & interpretations, and implicit evaluation. --- @@ -184,7 +196,7 @@ Requires Python 3.10–3.14. The core depends only on NumPy, nltk, and graphviz. --- -## Changelog & an experiment in AI-assisted algorithm engineering +## An experiment in AI-assisted algorithm engineering AutStr began in 2022 as a summer project — a hands-on realization of the automatic structures its author had studied during his PhD in algorithmic model theory. @@ -197,160 +209,79 @@ mathematical direction and review kept firmly human. alt="Gource animation of the AutStr commit history, showing the file tree growing across the human, DeepSeek and Claude phases">

-- **v1.0 (2022) — human.** The original library and arithmetic front-end. -- **v1.x (July 2025) — DeepSeek.** A vibe-coding session (with extensive human - testing and supervision) that added the sparse-DFA backend, serialization, and - the MSO0 finite-powerset structure, and modernized packaging. -- **v2.0 (July 2026) — Claude, Anthropic's Fable 5 model.** An intensive two-day - pair-programming session inside Claude Code that: - - profiled and rewrote the entire automata core as batched, sparsity-aware - NumPy — a **10²–10³× speedup** (the reference query dropped from 85 s to - 0.03 s), with linear memory; - - migrated the library from a hard JAX dependency to a NumPy-canonical core with - JAX as an optional accelerator; - - built the whole uniformly-automatic layer — the generic advice machinery, - bounded tree-depth and pathwidth graphs with MSO, finite Boolean algebras, - finite abelian groups, the ℤ[1/p] presentations, and the non-abelian group - classes — each verified against exhaustive or exact ground-truth oracles; - - added the [benchmark suite](benchmarks/) and these docs. - - The ideas realized in v2 include constructions the author had sketched a decade - earlier; several went from a whiteboard description to running, tested code - within hours. The code is the model's; the theory, the choices, and the - verification protocol were human. - -- **v3.0 (July 2026) — Claude, (various models)** A second session, in - the same protocol, that took the library from strings to trees and replaced the - transition representation underneath both: - - **tree-automatic structures.** `autstr.sparse_tree_automata` (bottom-up tree - automata), `autstr.tree_presentations`, and `autstr.tree_uniform` — the tree - counterparts of the whole stack. New members: **Skolem arithmetic** (ℕ, ·), - graphs of bounded **tree-width** and bounded **clique-width** with full MSO, - and tree-indexed **extraspecial p-groups**. Cross-validated by embedding the - string engine's Büchi arithmetic into the tree engine and re-deciding every - sentence through both. - - **transitions are shared multi-terminal BDDs** over the symbol's digits, in - both engines. `expand` became a variable renaming, `complement` stopped - touching diagrams at all, and `minimize` became one `apply` per state per - round. Queries that had been impossible for lack of alphabet width now - compile: an arity-5 relation over a 14-letter alphabet (14⁵ = 537 824 flat - symbols) went from *infeasible* to 0.2 s; tree-depth-4 bipartiteness from - 17 s to 0.4 s. The test suite went from ~2 min to ~35 s. - - - **composing presentations.** `autstr.composition`: disjoint union and - synchronous/asynchronous direct products of automatic structures, union of - uniformly automatic classes, and the direct-product closure of a class. - Composed, they present every finite direct product of index-≤2 cyclic groups - and extraspecial p-groups, drawn from either family — and decide that such a - product is abelian exactly when all of its factors are. - -- **v3.1 (July 2026) — Claude, Fable 5.** The rank-width release: new - mathematics on top of the v3 engines, in the same human-directed protocol. - - **class-2 groups of bounded rank-width.** `CutRankGroups` (linear layouts), - `CutRankTreeGroups` (tree layouts) and `CocycleRankWidthGroups` - (distributed centers, microcode advice) — the advice spells out rank-≤r - factorizations of the commutation form's crossing blocks, cut by cut. - - **the chain-ring extension.** Everything generalizes from F_p to - R = ℤ/pᵈ (`autstr.chain_ring`: Smith normal form, saturated interfaces, - the two-sided factorization lemma) — centers of exponent pᵈ, widths - measured as module cut-rank, byte-identical at d = 1. - - **factored advice letters.** Beyond ~20000 flat letters the cut-rank - classes stream one ring entry per letter through accumulator states, - making width r ≥ 2 over the ring representable (q+1 advice letters). - - **implicit evaluation.** `check_implicit` / `evaluate_implicit` on every - class: first-order model checking and satisfying-set computation that - never build a query — or even a base — automaton, reaching members (ℤ/8 - and ℤ/9 words, ℤ/4 trees, the distributed-center protocol) whose - automata are infeasible; `ImplicitClass` / `ImplicitTreeClass` are - presentations given purely by transition functions. - - **graphs of bounded rank-width.** `RankWidthClass` — rank decompositions - as advice, adjacency as a bilinear form on r-bit interface vectors, - full MSO; the graph face of the same linear algebra. - - Docs are built by CI with all notebooks **executed during the build** - (the repository keeps them output-free). - - One behavior change to a 3.0 API: `show_diagram` no longer opens an - external image viewer by default (headless builds must not spawn one); - pass `view=True` for the old behavior. +- **v1.0 (2022) — human.** The original library and arithmetic front end. +- **v1.x (2025) — DeepSeek.** A vibe-coding session, with extensive human + testing and supervision. +- **v2.0–v3.1 (2026) — Claude.** The automata core rewritten as batched, + sparsity-aware NumPy (10²–10³× faster); the uniformly-automatic layer; the + step from strings to trees; MTBDD transitions; the rank-width families. +- **v4.0 (2026) — Claude.** This release. + +Several of the constructions realized here were sketched by the author a decade +earlier and had never been implemented; some went from a whiteboard description +to running, tested code within hours. The code is the model's; the theory, the +choices, and the verification protocol are human. + +### What is new in v4.0 + +- **A symbolic first-order layer.** Write `(x + y).eq(z) & z.lt(100)` instead of + a formula string, over any structure or class, on either engine. Every + structure declares its own operators and its own **codec**, so Python values + go in and come out and `symbolic()` needs no arguments. +- **First-order interpretations** that *compute* the interpreted presentation, + quotients included — over trees too, where the representative of a class is + its least description rather than its least member. +- **Infinite graphs**: the integer grid, the regular tree, and Turing-machine + configuration graphs, where first-order logic stops exactly at reachability. +- **Level 2 collapsible pushdown graphs, with reachability.** Tree-automatic by + Kartzow's encoding, and `Reach` is a relation of the graph — so a first-order + formula may ask about runs of any length, which is precisely what the Turing + graph cannot be asked. +- **The countable atomless Boolean algebra**, and the ordinals below ω^ω and + ω^(ω^n). +- **Serialization for the tree engine**, so an expensive relation is built once + and kept. +- `autstr.buildin` is gone: every structure the library ships is built in, so + its contents moved to modules named for their subject. See the changelog for + the upgrade path. + +📜 **[Full changelog](CHANGELOG.md)** — every release, in detail. --- ## References -1. **Abu Zaid, F.** *Algorithmic Solutions via Model Theoretic Interpretations.* - Dissertation, RWTH Aachen University, 2016. - DOI: [10.18154/RWTH-2017-07663](https://doi.org/10.18154/RWTH-2017-07663) +AutStr implements a line of work that runs from Büchi's theorem to uniformly +automatic classes. The four below are the ones it leans on most; the +**[full bibliography](https://fariedabuzaid.github.io/AutStr/references.html)** +in the documentation lists the rest — Rabin, Courcelle, Delhommé, Kuske & +Weidner, Kartzow and others — and says for each what in the library it is. -2. **Abu Zaid, F.** *Uniformly Automatic Classes of Finite Structures.* - FSTTCS 2018, LIPIcs vol. 122, pp. 10:1–10:21. - DOI: [10.4230/LIPIcs.FSTTCS.2018.10](https://doi.org/10.4230/LIPIcs.FSTTCS.2018.10) - *The meta-theorems for finite Boolean algebras, finite groups, and graphs of - bounded tree-depth implemented by `autstr.uniform`, `autstr.graphs`, - `autstr.algebra`, and `autstr.groups`.* - -3. **Abu Zaid, F., Grädel, E., & Reinhardt, F.** *Advice Automatic Structures and - Uniformly Automatic Classes.* CSL 2017, LIPIcs vol. 82, pp. 35:1–35:20. - DOI: [10.4230/LIPIcs.CSL.2017.35](https://doi.org/10.4230/LIPIcs.CSL.2017.35) - *Introduces automatic presentations with advice — the foundation of the uniform - classes here; the ℤ[1/p] presentation follows its blueprint for (ℚ, +).* - -4. **Blumensath, A., & Grädel, E.** *Automatic Structures.* LICS 2000, pp. 51–62. - [Proceedings](https://lics.siglog.org/2000/Grdel-AutomaticStructures.html) +1. **Büchi, J. R.** *Weak Second-Order Arithmetic and Finite Automata.* + Zeitschrift für math. Logik und Grundlagen der Mathematik 6 (1960), 66–92. + DOI: [10.1002/malq.19600060105](https://doi.org/10.1002/malq.19600060105) + *Every `evaluate` call in this library is this construction.* -5. **Khoussainov, B., & Nerode, A.** *Automatic presentations of structures.* +2. **Khoussainov, B., & Nerode, A.** *Automatic presentations of structures.* LCC 1994, LNCS vol. 960, Springer. DOI: [10.1007/3-540-60178-3_93](https://doi.org/10.1007/3-540-60178-3_93) -6. **Khoussainov, B., Rubin, S., & Stephan, F.** *Automatic Structures: Richness - and Limitations.* LMCS 3(2), 2007. - arXiv: [cs/0703064](https://arxiv.org/abs/cs/0703064) · - DOI: [10.2168/LMCS-3(2:2)2007](https://doi.org/10.2168/LMCS-3%282%3A2%292007) - -### Foundations - -The idea that a logic can be decided by translating formulas into automata long -predates the term *automatic structure*; this library is a late implementation of -a line of work that runs through: +3. **Blumensath, A., & Grädel, E.** *Automatic Structures.* LICS 2000, pp. 51–62. + [Proceedings](https://lics.siglog.org/2000/Grdel-AutomaticStructures.html) + *Closure under first-order definability — the decidability `check` rests on.* -7. **Büchi, J. R.** *Weak Second-Order Arithmetic and Finite Automata.* - Zeitschrift für math. Logik und Grundlagen der Mathematik 6 (1960), 66–92. - DOI: [10.1002/malq.19600060105](https://doi.org/10.1002/malq.19600060105) - *Monadic second-order logic over (ℕ, +1) is decidable, by translation into - finite automata. Every `evaluate` call in this library is this construction.* - -8. **Rabin, M. O.** *Decidability of Second-Order Theories and Automata on - Infinite Trees.* Transactions of the AMS 141 (1969), 1–35. - DOI: [10.2307/1995086](https://doi.org/10.2307/1995086) - *The same programme over trees. `autstr.sparse_tree_automata` and the - tree-automatic presentations are the finite-tree fragment of this.* - -9. **Courcelle, B.** *The Monadic Second-Order Logic of Graphs I: Recognizable - Sets of Finite Graphs.* Information and Computation 85(1), 1990, 12–75. - DOI: [10.1016/0890-5401(90)90043-H](https://doi.org/10.1016/0890-5401%2890%2990043-H) - *MSO properties of graphs of bounded tree-width are decidable in linear time. - `autstr.tree_graphs.TreeWidthClass` builds the automaton the theorem promises.* - -10. **Courcelle, B., & Olariu, S.** *Upper Bounds to the Clique Width of Graphs.* - Discrete Applied Mathematics 101 (2000), 77–114. - DOI: [10.1016/S0166-218X(99)00184-5](https://doi.org/10.1016/S0166-218X%2899%2900184-5) - *The k-expressions that `autstr.tree_graphs.CliqueWidthClass` reads as advice.* - -11. **Makowsky, J. A.** *Algorithmic Uses of the Feferman–Vaught Theorem.* - Annals of Pure and Applied Logic 126 (2004), 159–213. - DOI: [10.1016/j.apal.2003.11.002](https://doi.org/10.1016/j.apal.2003.11.002) - *The composition method behind meta-theorems of this shape.* +4. **Abu Zaid, F.** *Uniformly Automatic Classes of Finite Structures.* + FSTTCS 2018, LIPIcs vol. 122, pp. 10:1–10:21. + DOI: [10.4230/LIPIcs.FSTTCS.2018.10](https://doi.org/10.4230/LIPIcs.FSTTCS.2018.10) + *The meta-theorems behind `autstr.uniform`, `autstr.graphs`, + `autstr.algebra` and `autstr.groups`.* ### Related tools -- **[MONA](https://www.brics.dk/mona/)** (Klarlund, Møller, Henriksen et al.) - decides WS1S and WS2S by translating formulas to automata whose transitions are - shared multi-terminal BDDs over the symbol's bits. AutStr's - [`autstr.mtbdd`](autstr/mtbdd.py) adopts exactly that representation, for - exactly MONA's reason: over a convolution alphabet, the flat - `symbol -> target` table is the bottleneck. -- **[Walnut](https://cs.uwaterloo.ca/~shallit/walnut.html)** (Mousavi, Shallit) - proves theorems about automatic sequences by deciding first-order statements - over (ℕ, +) with automata — the same decision procedure, aimed at combinatorics - on words rather than at presenting structures. - -Both are mature and fast, and neither targets *uniformly* automatic classes or -arbitrary automatic presentations, which is where AutStr sits. +**[MONA](https://www.brics.dk/mona/)** decides WS1S and WS2S with automata whose +transitions are shared multi-terminal BDDs over the symbol's bits; +[`autstr.mtbdd`](autstr/mtbdd.py) adopts exactly that representation, for +exactly MONA's reason. **[Walnut](https://cs.uwaterloo.ca/~shallit/walnut.html)** +proves theorems about automatic sequences by deciding first-order statements +over (ℕ, +). Both are mature and fast, and neither targets *uniformly* automatic +classes or arbitrary automatic presentations, which is where AutStr sits. diff --git a/autstr/_version.py b/autstr/_version.py index e276047..0951e03 100644 --- a/autstr/_version.py +++ b/autstr/_version.py @@ -1,2 +1,2 @@ # autstr/_version.py -__version__ = "3.1.0" +__version__ = "4.0.0" diff --git a/autstr/arithmetic.py b/autstr/arithmetic.py index d33a0f9..6f67499 100644 --- a/autstr/arithmetic.py +++ b/autstr/arithmetic.py @@ -1,85 +1,335 @@ -"""Büchi arithmetic over the integers, as a symbolic structure. +"""Büchi arithmetic, over the naturals and over the integers. -:math:`(\\mathbb{Z}, +, <, \\mid_2)` presented in base 2, with the generic -symbolic interface of `autstr.symbolic` on top: build terms and formulas with -Python operators, then evaluate, model check, test for emptiness or -finiteness, and enumerate solutions. +:math:`(\\mathbb{N}, +, <, \\mid_2)` and :math:`(\\mathbb{Z}, +, <, \\mid_2)` +presented in base 2, where ``x \\mid_2 y`` says that `y` is a power of two +dividing `x`. Adding that predicate to Presburger arithmetic is what makes the +structure *Büchi* arithmetic: it can talk about the binary expansion of a +number, and it remains decidable. - >>> Z = integers() + >>> Z = BuechiArithmeticZ().symbolic() >>> x, y, z = Z.vars("x y z") - >>> phi = (x + y).eq(z) & z.lt(100) - >>> phi.check() + >>> ((x + y).eq(z) & z.lt(100)).check() True - >>> phi.evaluate().contains(x=3, y=4, z=7) - True - -Integers are written directly wherever a term is expected -- ``x + 5``, -``x.lt(100)`` -- and solutions come back as Python integers. -The signature is that of the underlying presentation: ``A`` (addition graph), -``Lt``/``Gt``/``Eq``, ``Neg`` (the graph of negation), ``N0`` (non-negative), -``Z`` (zero), ``Pt`` (powers of two) and ``B``, where ``B(x, y)`` holds iff -``y`` is a power of two dividing ``x``. Anything the operators do not cover is -reachable through `SymbolicContext.rel`. +Both presentations are compiled from a handful of small automata the first time +they are constructed; the derived relations (order, equality, negation) are +first-order definitions over those. """ -from __future__ import annotations - -from functools import lru_cache from typing import List -from autstr.buildin.presentations import BuechiArithmeticZ -from autstr.symbolic import FunctionCodec, Signature, SymbolicContext - -#: Base-2 encoding: a sign symbol followed by the magnitude, least significant -#: bit first. This is the convention of `lsbf_Z_automaton`. -SIGN_POSITIVE = '0' -SIGN_NEGATIVE = '1' -PADDING = '*' - - -def encode(n: int) -> List[str]: - """The word encoding an integer: sign symbol, then magnitude bits LSB - first.""" - sign = SIGN_POSITIVE if n >= 0 else SIGN_NEGATIVE - return [sign] + list(format(abs(n), 'b')[::-1]) - - -def decode(word) -> int: - """The integer encoded by a word, ignoring padding.""" - word = ''.join(word).replace(PADDING, '') - if not word: - raise ValueError("empty encoding") - magnitude = int(word[1:][::-1] or '0', base=2) - return magnitude if word[0] == SIGN_POSITIVE else -magnitude - - -def signature() -> Signature: - """The signature of Büchi arithmetic: ``+`` and unary ``-`` as functions, - the order and equality as relational methods, and the integer codec.""" - sig = Signature(codec=FunctionCodec(encode, decode)) - sig.function('+', graph='A', out=2) - sig.function('neg', graph='Neg', out=1) - sig.operator('+', '+') - sig.operator('-', 'neg') - sig.operator('eq', 'Eq') - sig.operator('lt', 'Lt') - sig.operator('gt', 'Gt') - # B(x, y): y is a power of two dividing x. Spelled out as a method rather - # than bound to `|`, which on formulas already means union. - sig.operator('divided_by_power', 'B') - return sig - - -@lru_cache(maxsize=1) -def integers() -> SymbolicContext: - """The symbolic interface to Büchi arithmetic over :math:`\\mathbb{Z}`. - - The presentation is built once and shared; expressions are immutable, so - sharing it is safe and avoids rebuilding the base automata per term. +import itertools as it + +from autstr.presentations import ( + AutomaticPresentation, CompiledPresentation, +) +from autstr.utils.automata_tools import create_sparse_dfa + + +def _build_buechi_arithmetic() -> AutomaticPresentation: + """Büchi arithmetic over the natural numbers, compiled from scratch.""" + # Universe automaton - only accepts valid binary numbers (no '*') + universe = create_sparse_dfa( + states={'i', '0', '0+', '1', '*'}, + input_symbols={('0',), ('1',), ('*',)}, + transitions={ + 'i': {('0',): '0', ('1',): '1', ('*',): '*'}, + '0': {('0',): '0+', ('1',): '1', ('*',): '*'}, + '0+': {('0',): '0+', ('1',): '1', ('*',): '*'}, + '1': {('0',): '0+', ('1',): '1', ('*',): '*'}, + '*': {('0',): '*', ('1',): '*', ('*',): '*'}, + }, + initial_state='i', + final_states={'0', '1'} + ) + + addition = create_sparse_dfa( + states={0, 1, 2}, + input_symbols={('0', '0', '0'), ('0', '0', '1'), ('0', '0', '*'), ('0', '1', '0'), ('0', '1', '1'), + ('0', '1', '*'), ('0', '*', '0'), ('0', '*', '1'), ('0', '*', '*'), + ('1', '0', '0'), ('1', '0', '1'), ('1', '0', '*'), ('1', '1', '0'), ('1', '1', '1'), + ('1', '1', '*'), ('1', '*', '0'), ('1', '*', '1'), ('1', '*', '*'), + ('*', '0', '0'), ('*', '0', '1'), ('*', '0', '*'), ('*', '1', '0'), ('*', '1', '1'), + ('*', '1', '*'), ('*', '*', '0'), ('*', '*', '1'), ('*', '*', '*'), + }, + transitions={ + 0: { + ('0', '0', '0'): 0, ('0', '0', '1'): 2, ('0', '0', '*'): 2, ('0', '1', '0'): 2, ('0', '1', '1'): 0, + ('0', '1', '*'): 2, ('0', '*', '0'): 0, ('0', '*', '1'): 2, ('0', '*', '*'): 2, + ('1', '0', '0'): 2, ('1', '0', '1'): 0, ('1', '0', '*'): 2, ('1', '1', '0'): 1, ('1', '1', '1'): 2, + ('1', '1', '*'): 2, ('1', '*', '0'): 2, ('1', '*', '1'): 0, ('1', '*', '*'): 2, + ('*', '0', '0'): 0, ('*', '0', '1'): 2, ('*', '0', '*'): 2, ('*', '1', '0'): 2, ('*', '1', '1'): 0, + ('*', '1', '*'): 2, ('*', '*', '0'): 2, ('*', '*', '1'): 2, ('*', '*', '*'): 2, + }, + 1: { + ('0', '0', '0'): 2, ('0', '0', '1'): 0, ('0', '0', '*'): 2, ('0', '1', '0'): 1, ('0', '1', '1'): 2, + ('0', '1', '*'): 2, ('0', '*', '0'): 2, ('0', '*', '1'): 0, ('0', '*', '*'): 2, + ('1', '0', '0'): 1, ('1', '0', '1'): 2, ('1', '0', '*'): 2, ('1', '1', '0'): 2, ('1', '1', '1'): 1, + ('1', '1', '*'): 2, ('1', '*', '0'): 1, ('1', '*', '1'): 2, ('1', '*', '*'): 2, + ('*', '0', '0'): 2, ('*', '0', '1'): 0, ('*', '0', '*'): 2, ('*', '1', '0'): 1, ('*', '1', '1'): 2, + ('*', '1', '*'): 2, ('*', '*', '0'): 2, ('*', '*', '1'): 0, ('*', '*', '*'): 2, + }, + 2: { + ('0', '0', '0'): 2, ('0', '0', '1'): 2, ('0', '0', '*'): 2, ('0', '1', '0'): 2, ('0', '1', '1'): 2, + ('0', '1', '*'): 2, ('0', '*', '0'): 2, ('0', '*', '1'): 2, ('0', '*', '*'): 2, + ('1', '0', '0'): 2, ('1', '0', '1'): 2, ('1', '0', '*'): 2, ('1', '1', '0'): 2, ('1', '1', '1'): 2, + ('1', '1', '*'): 2, ('1', '*', '0'): 2, ('1', '*', '1'): 2, ('1', '*', '*'): 2, + ('*', '0', '0'): 2, ('*', '0', '1'): 2, ('*', '0', '*'): 2, ('*', '1', '0'): 2, ('*', '1', '1'): 2, + ('*', '1', '*'): 2, ('*', '*', '0'): 2, ('*', '*', '1'): 2, ('*', '*', '*'): 2, + }, + }, + initial_state=0, + final_states={0} + ) + + input_symbols = {a for a in it.product(['0', '1', '*'], repeat=2)} + weak_div = create_sparse_dfa( + states={'0', '1', 'e'}, + input_symbols=input_symbols, + transitions={ + '0': { + a: '0' if a == ('0', '0') else '1' if a == ('0', '1') or a == ('1', '1') else 'e' for a in input_symbols + }, + '1': { + a: 'e' if a[1] != '*' else '1' for a in input_symbols + }, + 'e': {a: 'e' for a in input_symbols} + }, + initial_state='0', + final_states={'1'} + ) + + + # Create presentation + presentation = AutomaticPresentation({'U': universe, 'A': addition, 'B': weak_div}) + + # Add bootstrap remaining relations + presentation.update(Z='A(x,x,x)') + presentation.update(Eq='exists z.(Z(z) and A(x,z,y))') + presentation.update(Pt='B(x,x)') + presentation.update(Lt='exists z.(not Z(z) and A(x, z, y))') + presentation.update(Gt='exists z.(not Z(z) and A(y, z, x))') + + return presentation + +def _build_buechi_arithmetic_Z() -> AutomaticPresentation: + """Büchi arithmetic over the integers, compiled from scratch.""" + # Universe automaton + universe_states = ['-1', 'i+', 'i', '0', '0+', '1', '*'] + universe_symbols = {('0',), ('1',), ('*',)} + universe_trans = { + '-1': {('0',): 'i', ('1',): 'i+', ('*',): '*'}, + 'i+': {('0',): '0+', ('1',): '1', ('*',): '*'}, + 'i': {('0',): '0', ('1',): '1', ('*',): '*'}, + '0': {('0',): '0+', ('1',): '1', ('*',): '*'}, + '0+': {('0',): '0+', ('1',): '1', ('*',): '*'}, + '1': {('0',): '0+', ('1',): '1', ('*',): '*'}, + '*': {('0',): '*', ('1',): '*', ('*',): '*'}, + } + universe = create_sparse_dfa( + universe_states, universe_symbols, universe_trans, '-1', {'0', '1'} + ) + + # Addition automaton (intermediate) + add_states = [-1, 0, 1, 2] + add_symbols = set(it.product(['0', '1', '*'], repeat=3)) + add_trans = { + -1: {a: 0 if '*' not in a else 2 for a in add_symbols}, + 0: { + ('0','0','0'): 0, ('0','0','1'): 2, ('0','0','*'): 2, + ('0','1','0'): 2, ('0','1','1'): 0, ('0','1','*'): 2, + ('0','*','0'): 0, ('0','*','1'): 2, ('0','*','*'): 2, + ('1','0','0'): 2, ('1','0','1'): 0, ('1','0','*'): 2, + ('1','1','0'): 1, ('1','1','1'): 2, ('1','1','*'): 2, + ('1','*','0'): 2, ('1','*','1'): 0, ('1','*','*'): 2, + ('*','0','0'): 0, ('*','0','1'): 2, ('*','0','*'): 2, + ('*','1','0'): 2, ('*','1','1'): 0, ('*','1','*'): 2, + ('*','*','0'): 2, ('*','*','1'): 2, ('*','*','*'): 2, + }, + 1: { + ('0','0','0'): 2, ('0','0','1'): 0, ('0','0','*'): 2, + ('0','1','0'): 1, ('0','1','1'): 2, ('0','1','*'): 2, + ('0','*','0'): 2, ('0','*','1'): 0, ('0','*','*'): 2, + ('1','0','0'): 1, ('1','0','1'): 2, ('1','0','*'): 2, + ('1','1','0'): 2, ('1','1','1'): 1, ('1','1','*'): 2, + ('1','*','0'): 1, ('1','*','1'): 2, ('1','*','*'): 2, + ('*','0','0'): 2, ('*','0','1'): 0, ('*','0','*'): 2, + ('*','1','0'): 1, ('*','1','1'): 2, ('*','1','*'): 2, + ('*','*','0'): 2, ('*','*','1'): 0, ('*','*','*'): 2, + }, + 2: {s: 2 for s in add_symbols} + } + addition_intermediate = create_sparse_dfa(add_states, add_symbols, add_trans, -1, {0}) + + # Weak division automaton + div_states = ['-1', '0', '1', 'e'] + div_symbols = set(it.product(['0', '1', '*'], repeat=2)) + div_trans = { + '-1': {a: '0' if a[1] == '0' else 'e' for a in div_symbols}, + '0': { + a: '0' if a == ('0','0') + else '1' if a in {('0','1'), ('1','1')} + else 'e' for a in div_symbols + }, + '1': { + a: 'e' if a[1] != '*' else '1' for a in div_symbols + }, + 'e': {a: 'e' for a in div_symbols} + } + weak_div = create_sparse_dfa(div_states, div_symbols, div_trans, '-1', {'1'}) + + # N0 automaton + n0_states = [-1, 0, 1] + n0_symbols = {('0',), ('1',), ('*',)} + n0_trans = { + -1: {('0',): 1, ('1',): 0, ('*',): 0}, + 0: {s: 0 for s in n0_symbols}, + 1: {s: 1 for s in n0_symbols} + } + N0 = create_sparse_dfa(n0_states, n0_symbols, n0_trans, -1, {1}) + + # Create presentation + presentation = AutomaticPresentation({ + 'U': universe, + 'A0': addition_intermediate, + 'B': weak_div, + 'N0': N0 + }) + presentation.update(Z='A0(x,x,x)') + + # Define addition formula + c000 = '(N0(x) and N0(y) and N0(z) and A0(x, y, z))' + c001 = '(N0(x) and N0(y) and not N0(z) and exists a z0.(Z(z0) and A0(x,y,a) and A0(a,z,z0)))' + c010 = '(N0(x) and not N0(y) and N0(z) and A0(z, y, x))' + c011 = '(N0(x) and not N0(y) and not N0(z) and A0(z, x, y))' + c100 = '(not N0(x) and N0(y) and N0(z) and A0(x, z, y))' + c101 = '(not N0(x) and N0(y) and not N0(z) and A0(z, y, x))' + c110 = '(not N0(x) and not N0(y) and N0(z) and exists a z0.(Z(z0) and A0(x,y,a) and A0(a,z,z0)))' + c111 = '(not N0(x) and not N0(y) and not N0(z) and A0(x,y,z))' + phi_A = ' or '.join([c000, c001, c010, c011, c100, c101, c110, c111]) + presentation.update(A=phi_A) + + presentation.update(Eq='exists z.(Z(z) and A(x,z,y))') + presentation.update(Pt='B(x,x) and N0(x)') + presentation.update(Lt='exists z.(N0(z) and not Z(z) and A(x, z, y))') + presentation.update(Gt='exists z.(N0(z) and not Z(z) and A(y, z, x))') + presentation.update(Neg='exists z.(Z(z) and A(x,y,z))') + + # Delete auxiliary relation + del presentation.automata['A0'] + + return presentation + + +# -------------------------------------------------------------------------- +# The presentations. Each declares its own vocabulary, so `symbolic()` takes +# no argument; see `CompiledPresentation`. +# -------------------------------------------------------------------------- + +class BuechiArithmetic(CompiledPresentation): + """Büchi arithmetic over the natural numbers: :math:`(\\mathbb{N}, +, <, + \\mid_2)` in base 2. + + >>> N = BuechiArithmetic() + >>> x, y = N.symbolic().vars("x y") + >>> ((x + y).eq(12) & x.lt(y)).check() + True + + ``B(x, y)`` holds iff `y` is a power of two dividing `x`; it is spelled + ``.divided_by_power`` rather than bound to ``|``, which on formulas already + means union. """ - return BuechiArithmeticZ().symbolic(signature()) + + _BUILD = staticmethod(_build_buechi_arithmetic) + + #: base-2 encoding: the magnitude, least significant bit first + PADDING = '*' + + @staticmethod + def encode(n: int) -> List[str]: + """The word encoding a natural number: binary, least significant bit + first.""" + if n < 0: + raise ValueError(f"not a natural number: {n}") + return list(format(n, 'b')[::-1]) + + @staticmethod + def decode(word) -> int: + """The natural number encoded by a word, ignoring padding.""" + digits = ''.join(word).replace(BuechiArithmetic.PADDING, '') + return int(digits[::-1] or '0', base=2) + + def default_signature(self): + """``+`` as addition, with the order, equality and divisibility as + methods, and naturals written as Python integers.""" + from autstr.symbolic import FunctionCodec, Signature + signature = Signature(codec=FunctionCodec(self.encode, self.decode)) + signature.function('+', graph='A', out=2) + signature.operator('+', '+') + signature.operator('eq', 'Eq') + signature.operator('lt', 'Lt') + signature.operator('gt', 'Gt') + signature.operator('divided_by_power', 'B') + return signature + + +class BuechiArithmeticZ(CompiledPresentation): + """Büchi arithmetic over the integers: :math:`(\\mathbb{Z}, +, <, \\mid_2)` + in base 2. + + >>> Z = BuechiArithmeticZ() + >>> x, y, z = Z.symbolic().vars("x y z") + >>> ((x + y).eq(z) & z.lt(100)).check() + True + >>> (3, 4, 7) in (x + y).eq(z) + True + + Integers are written directly wherever a term is expected -- ``x + 5``, + ``x.lt(100)`` -- and solutions come back as Python integers. Anything the + operators do not cover is reachable through `SymbolicContext.rel`. + """ + + _BUILD = staticmethod(_build_buechi_arithmetic_Z) + + #: base-2 encoding: a sign symbol, then the magnitude, least significant + #: bit first + SIGN_POSITIVE = '0' + SIGN_NEGATIVE = '1' + PADDING = '*' + + @staticmethod + def encode(n: int) -> List[str]: + """The word encoding an integer: sign symbol, then magnitude bits least + significant first.""" + sign = (BuechiArithmeticZ.SIGN_POSITIVE if n >= 0 + else BuechiArithmeticZ.SIGN_NEGATIVE) + return [sign] + list(format(abs(n), 'b')[::-1]) + + @staticmethod + def decode(word) -> int: + """The integer encoded by a word, ignoring padding.""" + word = ''.join(word).replace(BuechiArithmeticZ.PADDING, '') + if not word: + raise ValueError("empty encoding") + magnitude = int(word[1:][::-1] or '0', base=2) + return (magnitude if word[0] == BuechiArithmeticZ.SIGN_POSITIVE + else -magnitude) + + def default_signature(self): + """``+`` as addition and unary ``-`` as negation, with the order, + equality and divisibility as methods, and integers written as Python + integers.""" + from autstr.symbolic import FunctionCodec, Signature + signature = Signature(codec=FunctionCodec(self.encode, self.decode)) + signature.function('+', graph='A', out=2) + signature.function('neg', graph='Neg', out=1) + signature.operator('+', '+') + signature.operator('-', 'neg') + signature.operator('eq', 'Eq') + signature.operator('lt', 'Lt') + signature.operator('gt', 'Gt') + # B(x, y): y is a power of two dividing x. Spelled out as a method + # rather than bound to `|`, which on formulas already means union. + signature.operator('divided_by_power', 'B') + return signature -def variables(names) -> tuple: - """Shorthand for ``integers().vars(names)``.""" - return integers().vars(names) diff --git a/autstr/buildin/__init__.py b/autstr/buildin/__init__.py deleted file mode 100644 index e69de29..0000000 diff --git a/autstr/buildin/automata.py b/autstr/buildin/automata.py deleted file mode 100644 index f0844f6..0000000 --- a/autstr/buildin/automata.py +++ /dev/null @@ -1,138 +0,0 @@ -import itertools as it -from typing import Optional, Set -from autstr.sparse_automata import SparseDFA -import numpy as np - -from autstr.utils.misc import encode_symbol - -def length_automaton(n: int, base_alphabet: Set[int]) -> SparseDFA: - """ - Creates an automaton that recognizes all words over base_alphabet with length exactly n. - - :param n: The exact word length - :param base_alphabet: Set of integer symbols - :return: SparseDFA recognizing words of length n - """ - # States: 0 (start), 1, 2, ..., n (accepting), n+1 (dead) - num_states = n + 2 - # Default transitions: move to next state or dead state - default_states = np.array([i + 1 for i in range(n)] + [n + 1, n + 1], dtype=np.int32) - # No exceptions needed (same behavior for all symbols) - exception_symbols = np.full((num_states, 0), -1, dtype=np.int32) - exception_states = np.full((num_states, 0), -1, dtype=np.int32) - # Only state n is accepting - is_accepting = np.array([False] * n + [True, False]) - start_state = 0 - - return SparseDFA( - num_states=num_states, - default_states=default_states, - exception_symbols=exception_symbols, - exception_states=exception_states, - is_accepting=is_accepting, - start_state=start_state, - symbol_arity=1, - base_alphabet=base_alphabet - ) - -def k_longer_automaton(k: int, r: int, base_alphabet: Set[int], padding_symbol: int) -> SparseDFA: - """ - Creates an automaton recognizing (r+1)-tuples where the last word is at least k letters - longer than the other r words. - - :param k: Minimal length difference - :param r: Number of reference words - :param base_alphabet: Set of integer symbols - :param padding_symbol: Padding symbol integer - :return: SparseDFA for the k-longer condition - """ - # State mapping: [-1, 0, 1, ..., k] -> [0, 1, 2, ..., k+1] - state_mapping = {s: i for i, s in enumerate(range(-1, k+1))} - num_states = len(state_mapping) - sorted_alphabet = sorted(base_alphabet) - arity = r + 1 - - # Precompute all symbol tuples and their encodings - symbol_tuples = list(it.product(sorted_alphabet, repeat=arity)) - symbol_encodings = [encode_symbol(t, base_alphabet) for t in symbol_tuples] - - # Initialize DFA components - default_states = np.full(num_states, state_mapping[-1], dtype=np.int32) # Default to dead state - exception_list = [[] for _ in range(num_states)] - - # Build transitions - for state in range(-1, k+1): - state_idx = state_mapping[state] - for t, enc in zip(symbol_tuples, symbol_encodings): - # Compute next state - if state == -1: - next_state = -1 # Stay in dead state - else: - if all(x == padding_symbol for x in t[:-1]) and t[-1] != padding_symbol: - next_state = min(state + 1, k) # Count extra length - elif t[-1] == padding_symbol: - next_state = -1 # Reject if padding the last word - elif state == 0: - next_state = 0 # Wait for other words to end - else: - next_state = -1 # Reject otherwise - - next_state_idx = state_mapping[next_state] - if next_state_idx != state_mapping[-1]: - exception_list[state_idx].append((enc, next_state_idx)) - - # Find max exceptions needed - max_exceptions = max(len(ex_list) for ex_list in exception_list) if exception_list else 0 - - # Build exception arrays - exception_symbols = np.full((num_states, max_exceptions), -1, dtype=np.int32) - exception_states = np.full((num_states, max_exceptions), -1, dtype=np.int32) - - for i, ex_list in enumerate(exception_list): - if ex_list: - syms, states = zip(*ex_list) - exception_symbols[i, :len(syms)] = syms - exception_states[i, :len(states)] = states - - # Final states: state k (meaning we've counted k extra symbols) - is_accepting = np.array([i == state_mapping[k] for i in range(num_states)]) - - return SparseDFA( - num_states=num_states, - default_states=default_states, - exception_symbols=exception_symbols, - exception_states=exception_states, - is_accepting=is_accepting, - start_state=state_mapping[0], - symbol_arity=arity, - base_alphabet=base_alphabet - ) - - -def zero(symbol_arity: int = 1, base_alphabet: Optional[Set[int]] = None) -> SparseDFA: - """Automaton that rejects all inputs.""" - base_alphabet = base_alphabet or {0} - return SparseDFA( - num_states=1, - default_states=np.array([0], dtype=np.int32), - exception_symbols=np.full((1, 0), -1, dtype=np.int32), - exception_states=np.full((1, 0), -1, dtype=np.int32), - is_accepting=np.array([False]), - start_state=0, - symbol_arity=symbol_arity, - base_alphabet=base_alphabet - ) - -def one(symbol_arity: int = 1, base_alphabet: Optional[Set[int]] = None) -> SparseDFA: - """Automaton that accepts all inputs.""" - base_alphabet = base_alphabet or {0} - return SparseDFA( - num_states=1, - default_states=np.array([0], dtype=np.int32), - exception_symbols=np.full((1, 0), -1, dtype=np.int32), - exception_states=np.full((1, 0), -1, dtype=np.int32), - is_accepting=np.array([True]), - start_state=0, - symbol_arity=symbol_arity, - base_alphabet=base_alphabet - ) \ No newline at end of file diff --git a/autstr/buildin/bin/buechi.autstr b/autstr/buildin/bin/buechi.autstr deleted file mode 100644 index 24326b3..0000000 Binary files a/autstr/buildin/bin/buechi.autstr and /dev/null differ diff --git a/autstr/buildin/bin/buechiZ.autstr b/autstr/buildin/bin/buechiZ.autstr deleted file mode 100644 index f121de4..0000000 Binary files a/autstr/buildin/bin/buechiZ.autstr and /dev/null differ diff --git a/autstr/buildin/bin/mso0.autstr b/autstr/buildin/bin/mso0.autstr deleted file mode 100644 index c5274f1..0000000 Binary files a/autstr/buildin/bin/mso0.autstr and /dev/null differ diff --git a/autstr/buildin/presentations.py b/autstr/buildin/presentations.py deleted file mode 100644 index 480b9d9..0000000 --- a/autstr/buildin/presentations.py +++ /dev/null @@ -1,522 +0,0 @@ -from pathlib import Path -import itertools as it -from typing import Dict, List, Set, Tuple -import numpy as np - -from autstr.sparse_automata import SparseDFA -from autstr.presentations import AutomaticPresentation - - -# Helper function to convert a symbol tuple to an integer encoding -def encode_symbol(tup: Tuple[str], base_alphabet: Set[str]) -> int: - """Encode a symbol tuple into an integer using base conversion.""" - base = len(base_alphabet) - mapping = {sym: idx for idx, sym in enumerate(sorted(base_alphabet))} - enc = 0 - for char in tup: - enc = enc * base + mapping[char] - return enc - -# Helper function to create a SparseDFA from a traditional DFA description -def create_sparse_dfa(states: List[str], input_symbols: Set[Tuple[str]], - transitions: Dict[str, Dict[Tuple[str], str]], - initial_state: str, final_states: Set[str]) -> SparseDFA: - """Convert a traditional DFA description to a SparseDFA.""" - # Map states to integers - state_to_index = {s: i for i, s in enumerate(states)} - num_states = len(states) - - # Determine base alphabet and arity - base_alphabet = set() - for sym in input_symbols: - for char in sym: - base_alphabet.add(char) - arity = len(next(iter(input_symbols))) if input_symbols else 0 - - # Create state arrays - default_states = [] - exception_symbols = [] - exception_states = [] - is_accepting = np.array([state in final_states for state in states], dtype=bool) - - # Build symbol mapping - symbol_map = {} - for symbol in input_symbols: - symbol_map[symbol] = encode_symbol(symbol, base_alphabet) - - # Process each state - for state in states: - # Find most common transition - next_states = [transitions[state][sym] for sym in input_symbols] - default_target = max(set(next_states), key=next_states.count) - default_states.append(state_to_index[default_target]) - - # Collect exceptions - exceptions = [] - for symbol, next_state in transitions[state].items(): - if next_state != default_target: - sym_enc = symbol_map[symbol] - next_idx = state_to_index[next_state] - exceptions.append((sym_enc, next_idx)) - - # Sort exceptions by symbol for consistency - exceptions.sort(key=lambda x: x[0]) - exception_symbols.append([e[0] for e in exceptions]) - exception_states.append([e[1] for e in exceptions]) - - # Pad exceptions - max_exceptions = max(len(e) for e in exception_symbols) if exception_symbols else 0 - padded_ex_syms = np.full((num_states, max_exceptions), -1, dtype=np.int32) - padded_ex_states = np.full((num_states, max_exceptions), -1, dtype=np.int32) - - for i in range(num_states): - if exception_symbols[i]: - padded_ex_syms[i, :len(exception_symbols[i])] = exception_symbols[i] - padded_ex_states[i, :len(exception_states[i])] = exception_states[i] - - return SparseDFA( - num_states=num_states, - default_states=np.array(default_states, dtype=np.int32), - exception_symbols=padded_ex_syms, - exception_states=padded_ex_states, - is_accepting=is_accepting, - start_state=state_to_index[initial_state], - symbol_arity=arity, - base_alphabet=base_alphabet - ).minimize() - -def BuechiArithmetic() -> AutomaticPresentation: - """Load the serialized Büchi arithmetic presentation.""" - current_dir = Path(__file__).parent - bin_path = current_dir / 'bin' / 'buechi.autstr' - return AutomaticPresentation.automatic_presentation_from_file(str(bin_path)) - -def buechi_arithmetic() -> AutomaticPresentation: - """Sparse version of Büchi arithmetic over natural numbers. Compiles definable relation from scratch.""" - # Universe automaton - only accepts valid binary numbers (no '*') - universe = create_sparse_dfa( - states={'i', '0', '0+', '1', '*'}, - input_symbols={('0',), ('1',), ('*',)}, - transitions={ - 'i': {('0',): '0', ('1',): '1', ('*',): '*'}, - '0': {('0',): '0+', ('1',): '1', ('*',): '*'}, - '0+': {('0',): '0+', ('1',): '1', ('*',): '*'}, - '1': {('0',): '0+', ('1',): '1', ('*',): '*'}, - '*': {('0',): '*', ('1',): '*', ('*',): '*'}, - }, - initial_state='i', - final_states={'0', '1'} - ) - - addition = create_sparse_dfa( - states={0, 1, 2}, - input_symbols={('0', '0', '0'), ('0', '0', '1'), ('0', '0', '*'), ('0', '1', '0'), ('0', '1', '1'), - ('0', '1', '*'), ('0', '*', '0'), ('0', '*', '1'), ('0', '*', '*'), - ('1', '0', '0'), ('1', '0', '1'), ('1', '0', '*'), ('1', '1', '0'), ('1', '1', '1'), - ('1', '1', '*'), ('1', '*', '0'), ('1', '*', '1'), ('1', '*', '*'), - ('*', '0', '0'), ('*', '0', '1'), ('*', '0', '*'), ('*', '1', '0'), ('*', '1', '1'), - ('*', '1', '*'), ('*', '*', '0'), ('*', '*', '1'), ('*', '*', '*'), - }, - transitions={ - 0: { - ('0', '0', '0'): 0, ('0', '0', '1'): 2, ('0', '0', '*'): 2, ('0', '1', '0'): 2, ('0', '1', '1'): 0, - ('0', '1', '*'): 2, ('0', '*', '0'): 0, ('0', '*', '1'): 2, ('0', '*', '*'): 2, - ('1', '0', '0'): 2, ('1', '0', '1'): 0, ('1', '0', '*'): 2, ('1', '1', '0'): 1, ('1', '1', '1'): 2, - ('1', '1', '*'): 2, ('1', '*', '0'): 2, ('1', '*', '1'): 0, ('1', '*', '*'): 2, - ('*', '0', '0'): 0, ('*', '0', '1'): 2, ('*', '0', '*'): 2, ('*', '1', '0'): 2, ('*', '1', '1'): 0, - ('*', '1', '*'): 2, ('*', '*', '0'): 2, ('*', '*', '1'): 2, ('*', '*', '*'): 2, - }, - 1: { - ('0', '0', '0'): 2, ('0', '0', '1'): 0, ('0', '0', '*'): 2, ('0', '1', '0'): 1, ('0', '1', '1'): 2, - ('0', '1', '*'): 2, ('0', '*', '0'): 2, ('0', '*', '1'): 0, ('0', '*', '*'): 2, - ('1', '0', '0'): 1, ('1', '0', '1'): 2, ('1', '0', '*'): 2, ('1', '1', '0'): 2, ('1', '1', '1'): 1, - ('1', '1', '*'): 2, ('1', '*', '0'): 1, ('1', '*', '1'): 2, ('1', '*', '*'): 2, - ('*', '0', '0'): 2, ('*', '0', '1'): 0, ('*', '0', '*'): 2, ('*', '1', '0'): 1, ('*', '1', '1'): 2, - ('*', '1', '*'): 2, ('*', '*', '0'): 2, ('*', '*', '1'): 0, ('*', '*', '*'): 2, - }, - 2: { - ('0', '0', '0'): 2, ('0', '0', '1'): 2, ('0', '0', '*'): 2, ('0', '1', '0'): 2, ('0', '1', '1'): 2, - ('0', '1', '*'): 2, ('0', '*', '0'): 2, ('0', '*', '1'): 2, ('0', '*', '*'): 2, - ('1', '0', '0'): 2, ('1', '0', '1'): 2, ('1', '0', '*'): 2, ('1', '1', '0'): 2, ('1', '1', '1'): 2, - ('1', '1', '*'): 2, ('1', '*', '0'): 2, ('1', '*', '1'): 2, ('1', '*', '*'): 2, - ('*', '0', '0'): 2, ('*', '0', '1'): 2, ('*', '0', '*'): 2, ('*', '1', '0'): 2, ('*', '1', '1'): 2, - ('*', '1', '*'): 2, ('*', '*', '0'): 2, ('*', '*', '1'): 2, ('*', '*', '*'): 2, - }, - }, - initial_state=0, - final_states={0} - ) - - input_symbols = {a for a in it.product(['0', '1', '*'], repeat=2)} - weak_div = create_sparse_dfa( - states={'0', '1', 'e'}, - input_symbols=input_symbols, - transitions={ - '0': { - a: '0' if a == ('0', '0') else '1' if a == ('0', '1') or a == ('1', '1') else 'e' for a in input_symbols - }, - '1': { - a: 'e' if a[1] != '*' else '1' for a in input_symbols - }, - 'e': {a: 'e' for a in input_symbols} - }, - initial_state='0', - final_states={'1'} - ) - - - # Create presentation - presentation = AutomaticPresentation({'U': universe, 'A': addition, 'B': weak_div}) - - # Add bootstrap remaining relations - presentation.update(Z='A(x,x,x)') - presentation.update(Eq='exists z.(Z(z) and A(x,z,y))') - presentation.update(Pt='B(x,x)') - presentation.update(Lt='exists z.(not Z(z) and A(x, z, y))') - presentation.update(Gt='exists z.(not Z(z) and A(y, z, x))') - - return presentation - -def BuechiArithmeticZ() -> AutomaticPresentation: - """Load the serialized Büchi arithmetic presentation.""" - current_dir = Path(__file__).parent - bin_path = current_dir / 'bin' / 'buechiZ.autstr' - return AutomaticPresentation.automatic_presentation_from_file(str(bin_path)) - -def buechi_arithmetic_Z() -> AutomaticPresentation: - """Sparse version of Büchi arithmetic over integers.""" - # Universe automaton - universe_states = ['-1', 'i+', 'i', '0', '0+', '1', '*'] - universe_symbols = {('0',), ('1',), ('*',)} - universe_trans = { - '-1': {('0',): 'i', ('1',): 'i+', ('*',): '*'}, - 'i+': {('0',): '0+', ('1',): '1', ('*',): '*'}, - 'i': {('0',): '0', ('1',): '1', ('*',): '*'}, - '0': {('0',): '0+', ('1',): '1', ('*',): '*'}, - '0+': {('0',): '0+', ('1',): '1', ('*',): '*'}, - '1': {('0',): '0+', ('1',): '1', ('*',): '*'}, - '*': {('0',): '*', ('1',): '*', ('*',): '*'}, - } - universe = create_sparse_dfa( - universe_states, universe_symbols, universe_trans, '-1', {'0', '1'} - ) - - # Addition automaton (intermediate) - add_states = [-1, 0, 1, 2] - add_symbols = set(it.product(['0', '1', '*'], repeat=3)) - add_trans = { - -1: {a: 0 if '*' not in a else 2 for a in add_symbols}, - 0: { - ('0','0','0'): 0, ('0','0','1'): 2, ('0','0','*'): 2, - ('0','1','0'): 2, ('0','1','1'): 0, ('0','1','*'): 2, - ('0','*','0'): 0, ('0','*','1'): 2, ('0','*','*'): 2, - ('1','0','0'): 2, ('1','0','1'): 0, ('1','0','*'): 2, - ('1','1','0'): 1, ('1','1','1'): 2, ('1','1','*'): 2, - ('1','*','0'): 2, ('1','*','1'): 0, ('1','*','*'): 2, - ('*','0','0'): 0, ('*','0','1'): 2, ('*','0','*'): 2, - ('*','1','0'): 2, ('*','1','1'): 0, ('*','1','*'): 2, - ('*','*','0'): 2, ('*','*','1'): 2, ('*','*','*'): 2, - }, - 1: { - ('0','0','0'): 2, ('0','0','1'): 0, ('0','0','*'): 2, - ('0','1','0'): 1, ('0','1','1'): 2, ('0','1','*'): 2, - ('0','*','0'): 2, ('0','*','1'): 0, ('0','*','*'): 2, - ('1','0','0'): 1, ('1','0','1'): 2, ('1','0','*'): 2, - ('1','1','0'): 2, ('1','1','1'): 1, ('1','1','*'): 2, - ('1','*','0'): 1, ('1','*','1'): 2, ('1','*','*'): 2, - ('*','0','0'): 2, ('*','0','1'): 0, ('*','0','*'): 2, - ('*','1','0'): 1, ('*','1','1'): 2, ('*','1','*'): 2, - ('*','*','0'): 2, ('*','*','1'): 0, ('*','*','*'): 2, - }, - 2: {s: 2 for s in add_symbols} - } - addition_intermediate = create_sparse_dfa(add_states, add_symbols, add_trans, -1, {0}) - - # Weak division automaton - div_states = ['-1', '0', '1', 'e'] - div_symbols = set(it.product(['0', '1', '*'], repeat=2)) - div_trans = { - '-1': {a: '0' if a[1] == '0' else 'e' for a in div_symbols}, - '0': { - a: '0' if a == ('0','0') - else '1' if a in {('0','1'), ('1','1')} - else 'e' for a in div_symbols - }, - '1': { - a: 'e' if a[1] != '*' else '1' for a in div_symbols - }, - 'e': {a: 'e' for a in div_symbols} - } - weak_div = create_sparse_dfa(div_states, div_symbols, div_trans, '-1', {'1'}) - - # N0 automaton - n0_states = [-1, 0, 1] - n0_symbols = {('0',), ('1',), ('*',)} - n0_trans = { - -1: {('0',): 1, ('1',): 0, ('*',): 0}, - 0: {s: 0 for s in n0_symbols}, - 1: {s: 1 for s in n0_symbols} - } - N0 = create_sparse_dfa(n0_states, n0_symbols, n0_trans, -1, {1}) - - # Create presentation - presentation = AutomaticPresentation({ - 'U': universe, - 'A0': addition_intermediate, - 'B': weak_div, - 'N0': N0 - }) - presentation.update(Z='A0(x,x,x)') - - # Define addition formula - c000 = '(N0(x) and N0(y) and N0(z) and A0(x, y, z))' - c001 = '(N0(x) and N0(y) and not N0(z) and exists a z0.(Z(z0) and A0(x,y,a) and A0(a,z,z0)))' - c010 = '(N0(x) and not N0(y) and N0(z) and A0(z, y, x))' - c011 = '(N0(x) and not N0(y) and not N0(z) and A0(z, x, y))' - c100 = '(not N0(x) and N0(y) and N0(z) and A0(x, z, y))' - c101 = '(not N0(x) and N0(y) and not N0(z) and A0(z, y, x))' - c110 = '(not N0(x) and not N0(y) and N0(z) and exists a z0.(Z(z0) and A0(x,y,a) and A0(a,z,z0)))' - c111 = '(not N0(x) and not N0(y) and not N0(z) and A0(x,y,z))' - phi_A = ' or '.join([c000, c001, c010, c011, c100, c101, c110, c111]) - presentation.update(A=phi_A) - - presentation.update(Eq='exists z.(Z(z) and A(x,z,y))') - presentation.update(Pt='B(x,x) and N0(x)') - presentation.update(Lt='exists z.(N0(z) and not Z(z) and A(x, z, y))') - presentation.update(Gt='exists z.(N0(z) and not Z(z) and A(y, z, x))') - presentation.update(Neg='exists z.(Z(z) and A(x,y,z))') - - # Delete auxiliary relation - del presentation.automata['A0'] - - return presentation - -def MSO0() -> AutomaticPresentation: - """Load the serialized MSO0 presentation.""" - current_dir = Path(__file__).parent - bin_path = current_dir / 'bin' / 'mso0.autstr' - return AutomaticPresentation.automatic_presentation_from_file(str(bin_path)) - -def finite_powerset() -> AutomaticPresentation: - # Base alphabet for the presentation - base_alphabet = {'0', '1', '*'} - - # 1. Universe Automaton (U) - Includes empty set - universe = create_sparse_dfa( - states={'start', 'empty', 'zero', 'one', 'pad_one', 'pad_zero', 'reject'}, - input_symbols={'0', '1', '*'}, - transitions={ - 'start': { - '*': 'empty', - '0': 'zero', - '1': 'one' - }, - 'empty': { - '*': 'empty', - '0': 'reject', - '1': 'reject' - }, - 'zero': { - '*': 'pad_zero', - '0': 'zero', - '1': 'one' - }, - 'one': { - '*': 'pad_one', - '0': 'zero', - '1': 'one' - }, - 'pad_zero': { - '*': 'pad_zero', - '0': 'reject', - '1': 'reject' - }, - 'pad_one': { - '*': 'pad_one', - '0': 'reject', - '1': 'reject' - }, - 'reject': { - '0': 'reject', - '1': 'reject', - '*': 'reject' - } - }, - initial_state='start', - final_states={'start', 'one','empty', 'pad_one'} # Accepts empty set and non-empty sets - ) - - # 2. Subset Automaton (Subset) - Empty set is subset of all sets - subset = create_sparse_dfa( - states={'start', 'error'}, - input_symbols=set(it.product(base_alphabet, repeat=2)), - transitions={ - 'start': { - ('0','0'): 'start', - ('0','1'): 'start', - ('0','*'): 'start', - ('1','1'): 'start', - ('*','0'): 'start', - ('*','1'): 'start', - ('*','*'): 'start', - ('1','0'): 'error', - ('1','*'): 'error' - }, - 'error': {k: 'error' for k in it.product(base_alphabet, repeat=2)} - }, - initial_state='start', - final_states={'start'} - ) - - # 3. Singleton Automaton (Sing) - Empty set is not a singleton - sing = create_sparse_dfa( - states={'start', 'one', 'one_pad', 'many', 'reject'}, - input_symbols=base_alphabet, - transitions={ - 'start': { - '0': 'start', - '1': 'one', - '*': 'reject' # Reject empty set immediately - }, - 'one': { - '0': 'reject', - '1': 'many', - '*': 'one_pad' - }, - 'one_pad': { - '0': 'many', - '1': 'many', - '*': 'one_pad' - }, - 'many': { - '0': 'many', - '1': 'many', - '*': 'many' - }, - 'reject': { - '0': 'reject', - '1': 'reject', - '*': 'reject' - } - }, - initial_state='start', - final_states={'one','one_pad'} # Only non-empty singletons - ) - - # 4. Successor Automaton (Succ) - Empty set has no successor - succ = create_sparse_dfa( - states={'start', 'after_x', 'after_y', 'error'}, - input_symbols=set(it.product(base_alphabet, repeat=2)), - transitions={ - 'start': { - ('0','0'): 'start', - ('1','0'): 'after_x', - ('0','1'): 'error', - ('1','1'): 'error', - ('*','*'): 'error', # Reject empty set - ('0','*'): 'error', - ('1','*'): 'error', - ('*','0'): 'error', - ('*','1'): 'error' - }, - 'after_x': { - ('*','1'): 'after_y', - ('0','0'): 'error', - ('0','1'): 'error', - ('1','0'): 'error', - ('1','1'): 'error', - ('*','0'): 'error', - ('0','*'): 'error', - ('1','*'): 'error', - ('*','*'): 'error' - }, - 'after_y': { - ('*','*'): 'after_y', - ('0','0'): 'error', - ('0','1'): 'error', - ('1','0'): 'error', - ('1','1'): 'error', - ('*','0'): 'error', - ('*','1'): 'error', - ('0','*'): 'error', - ('1','*'): 'error' - }, - 'error': {k: 'error' for k in it.product(base_alphabet, repeat=2)} - }, - initial_state='start', - final_states={'after_y'} # Only consecutive singletons - ) - - # 5. Less-Than on Singletons Automaton (Lt_sing) - Empty set not involved - lt_sing = create_sparse_dfa( - states={'init', 'x_first', 'x_first_accept', 'error'}, - input_symbols=set(it.product(base_alphabet, repeat=2)), - transitions={ - 'init': { - ('0','0'): 'init', - ('0','1'): 'error', - ('1','0'): 'x_first', - ('1','1'): 'error', - ('*','*'): 'error', - ('0','*'): 'error', - ('*','0'): 'error', - ('1','*'): 'error', - ('*','1'): 'error' - }, - 'x_first': { - ('0','0'): 'x_first', - ('0','1'): 'x_first_accept', - ('1','0'): 'error', - ('1','1'): 'error', - ('*','*'): 'error', - ('0','*'): 'error', - ('*','0'): 'x_first', - ('1','*'): 'error', - ('*','1'): 'x_first_accept' - }, - 'x_first_accept': { - ('*','*'): 'x_first_accept', - ('0','0'): 'error', - ('0','1'): 'error', - ('1','0'): 'error', - ('1','1'): 'error', - ('*','0'): 'error', - ('*','1'): 'error', - ('0','*'): 'error', - ('1','*'): 'error' - }, - 'error': {k: 'error' for k in it.product(base_alphabet, repeat=2)} - }, - initial_state='init', - final_states={'x_first_accept'} # Only when first singleton < second - ) - - # Create the presentation with base automata - presentation = AutomaticPresentation({ - 'U': universe, - 'Subset': subset, - 'Sing': sing, - 'Succ': succ, - 'Lt_sing': lt_sing - }) - - # Define additional relations using formulas - presentation.update( - In="Sing(x) and Subset(x, y)", - Eq_set="Subset(x, y) and Subset(y, x)", - Leq_sing="Lt_sing(x, y) or (Eq_set(x, y) and Sing(x) and Sing(y))", - Gt_sing="not Leq_sing(x, y) and Sing(x) and Sing(y)", - Min="(forall z. not Subset(z, x)) or " # Empty set case - "(Sing(y) and Subset(y, x) and forall z. (-(Sing(z) and Subset(z, x)) or Leq_sing(y, z)))", - Max="Sing(y) and Subset(y, x) and forall z. (-(Sing(z) and Subset(z, x)) or Leq_sing(z, y))", - Intersect="forall a. (-Sing(a) or ((Subset(a, z) and (Subset(a, x) and Subset(a, y))) or (-Subset(a, z) and -(Subset(a, x) and Subset(a, y)))))", - Union="forall a. (-Sing(a) or ((Subset(a, z) and (Subset(a, x) or Subset(a, y))) or (-Subset(a, z) and -(Subset(a, x) or Subset(a, y)))))", - SetMinus="forall a. (-Sing(a) or ((Subset(a, z) and (Subset(a, x) and not Subset(a, y))) or (-Subset(a, z) and -(Subset(a, x) and not Subset(a, y)))))" - ) - - presentation.update( - Geq_sing="not Lt_sing(x, y) and Sing(x) and Sing(y)", - ) - - return presentation - diff --git a/autstr/collapsible.py b/autstr/collapsible.py index aadfc2b..7bed383 100644 --- a/autstr/collapsible.py +++ b/autstr/collapsible.py @@ -1028,8 +1028,9 @@ def get_relation_symbols(self): return self.presentation.get_relation_symbols() def is_deterministic(self) -> bool: - """Whether every configuration has at most one successor — first-order, - and so decidable, even though reachability is not built here.""" + """Whether every configuration has at most one successor — a + first-order property of the one-step relation, so it costs nothing + beyond `E`.""" return self.presentation.check( 'all x.(all y.(all z.((E(x,y) & E(x,z)) -> Eq(y,z))))') diff --git a/autstr/infinite_graphs.py b/autstr/infinite_graphs.py index 791af59..74b8ae1 100644 --- a/autstr/infinite_graphs.py +++ b/autstr/infinite_graphs.py @@ -135,7 +135,7 @@ def _path(): """The two-way integer path as a minimal presentation carrying only the domain, the ±1 edge, and equality — so the product folds those and nothing else.""" - from autstr.buildin.presentations import BuechiArithmeticZ + from autstr.arithmetic import BuechiArithmeticZ from autstr.presentations import AutomaticPresentation z = BuechiArithmeticZ() z.update(E=f'exists o.(({_ONE}) & (A(x,o,y) | A(y,o,x)))') @@ -145,7 +145,8 @@ def _path(): # -- element codec: an n-tuple <-> its nested-pair convolution ------ def encode(self, point: Sequence[int]) -> list: - from autstr.arithmetic import encode as encode_int + from autstr.arithmetic import BuechiArithmeticZ + encode_int = BuechiArithmeticZ.encode point = tuple(point) if len(point) != self.n: raise ValueError(f"expected a {self.n}-tuple, got {point!r}") @@ -161,7 +162,8 @@ def encode(self, point: Sequence[int]) -> list: return word def decode(self, word) -> Tuple[int, ...]: - from autstr.arithmetic import decode as decode_int + from autstr.arithmetic import BuechiArithmeticZ + decode_int = BuechiArithmeticZ.decode coordinates = [] current = list(word) for _ in range(self.n - 1): diff --git a/autstr/ordinals.py b/autstr/ordinals.py index 776fd11..283f3b4 100644 --- a/autstr/ordinals.py +++ b/autstr/ordinals.py @@ -43,7 +43,7 @@ from typing import Dict, List, Mapping, Optional, Sequence, Tuple, Union -from autstr.buildin.presentations import BuechiArithmetic +from autstr.arithmetic import BuechiArithmetic from autstr.interpretations import interpret from autstr.sparse_tree_automata import SparseTreeAutomaton, Tree from autstr.symbolic import FunctionCodec, order_signature diff --git a/autstr/powerset.py b/autstr/powerset.py new file mode 100644 index 0000000..2f35394 --- /dev/null +++ b/autstr/powerset.py @@ -0,0 +1,319 @@ +"""The finite subsets of the naturals -- the structure MSO0. + +Finite subsets of :math:`\\mathbb{N}` under :math:`\\subseteq`, with singletons, +the successor on singletons and their order. A finite set is a +:math:`\\{0,1\\}`-word, position `i` set iff `i` is a member, so by Büchi's +theorem first-order logic over this structure is exactly **monadic second-order +logic** over :math:`(\\mathbb{N}, <)`: the definable sets of naturals are +precisely the regular ones. + + >>> M = MSO0().symbolic() + >>> x, y = M.vars("x y") + >>> ({0, 2}, {0, 1, 2}) in x.subset(y) + True + +That correspondence is why the structure is called MSO0, and why quantifying +over sets here costs no more than quantifying over elements elsewhere. +""" +from typing import List + +import itertools as it + +from autstr.presentations import ( + AutomaticPresentation, CompiledPresentation, +) +from autstr.utils.automata_tools import create_sparse_dfa + + +def _build_finite_powerset() -> AutomaticPresentation: + """The finite subsets of the naturals, compiled from scratch.""" + # Base alphabet for the presentation + base_alphabet = {'0', '1', '*'} + + # 1. Universe Automaton (U) - Includes empty set + universe = create_sparse_dfa( + states={'start', 'empty', 'zero', 'one', 'pad_one', 'pad_zero', 'reject'}, + input_symbols={'0', '1', '*'}, + transitions={ + 'start': { + '*': 'empty', + '0': 'zero', + '1': 'one' + }, + 'empty': { + '*': 'empty', + '0': 'reject', + '1': 'reject' + }, + 'zero': { + '*': 'pad_zero', + '0': 'zero', + '1': 'one' + }, + 'one': { + '*': 'pad_one', + '0': 'zero', + '1': 'one' + }, + 'pad_zero': { + '*': 'pad_zero', + '0': 'reject', + '1': 'reject' + }, + 'pad_one': { + '*': 'pad_one', + '0': 'reject', + '1': 'reject' + }, + 'reject': { + '0': 'reject', + '1': 'reject', + '*': 'reject' + } + }, + initial_state='start', + final_states={'start', 'one','empty', 'pad_one'} # Accepts empty set and non-empty sets + ) + + # 2. Subset Automaton (Subset) - Empty set is subset of all sets + subset = create_sparse_dfa( + states={'start', 'error'}, + input_symbols=set(it.product(base_alphabet, repeat=2)), + transitions={ + 'start': { + ('0','0'): 'start', + ('0','1'): 'start', + ('0','*'): 'start', + ('1','1'): 'start', + ('*','0'): 'start', + ('*','1'): 'start', + ('*','*'): 'start', + ('1','0'): 'error', + ('1','*'): 'error' + }, + 'error': {k: 'error' for k in it.product(base_alphabet, repeat=2)} + }, + initial_state='start', + final_states={'start'} + ) + + # 3. Singleton Automaton (Sing) - Empty set is not a singleton + sing = create_sparse_dfa( + states={'start', 'one', 'one_pad', 'many', 'reject'}, + input_symbols=base_alphabet, + transitions={ + 'start': { + '0': 'start', + '1': 'one', + '*': 'reject' # Reject empty set immediately + }, + 'one': { + '0': 'reject', + '1': 'many', + '*': 'one_pad' + }, + 'one_pad': { + '0': 'many', + '1': 'many', + '*': 'one_pad' + }, + 'many': { + '0': 'many', + '1': 'many', + '*': 'many' + }, + 'reject': { + '0': 'reject', + '1': 'reject', + '*': 'reject' + } + }, + initial_state='start', + final_states={'one','one_pad'} # Only non-empty singletons + ) + + # 4. Successor Automaton (Succ) - Empty set has no successor + succ = create_sparse_dfa( + states={'start', 'after_x', 'after_y', 'error'}, + input_symbols=set(it.product(base_alphabet, repeat=2)), + transitions={ + 'start': { + ('0','0'): 'start', + ('1','0'): 'after_x', + ('0','1'): 'error', + ('1','1'): 'error', + ('*','*'): 'error', # Reject empty set + ('0','*'): 'error', + ('1','*'): 'error', + ('*','0'): 'error', + ('*','1'): 'error' + }, + 'after_x': { + ('*','1'): 'after_y', + ('0','0'): 'error', + ('0','1'): 'error', + ('1','0'): 'error', + ('1','1'): 'error', + ('*','0'): 'error', + ('0','*'): 'error', + ('1','*'): 'error', + ('*','*'): 'error' + }, + 'after_y': { + ('*','*'): 'after_y', + ('0','0'): 'error', + ('0','1'): 'error', + ('1','0'): 'error', + ('1','1'): 'error', + ('*','0'): 'error', + ('*','1'): 'error', + ('0','*'): 'error', + ('1','*'): 'error' + }, + 'error': {k: 'error' for k in it.product(base_alphabet, repeat=2)} + }, + initial_state='start', + final_states={'after_y'} # Only consecutive singletons + ) + + # 5. Less-Than on Singletons Automaton (Lt_sing) - Empty set not involved + lt_sing = create_sparse_dfa( + states={'init', 'x_first', 'x_first_accept', 'error'}, + input_symbols=set(it.product(base_alphabet, repeat=2)), + transitions={ + 'init': { + ('0','0'): 'init', + ('0','1'): 'error', + ('1','0'): 'x_first', + ('1','1'): 'error', + ('*','*'): 'error', + ('0','*'): 'error', + ('*','0'): 'error', + ('1','*'): 'error', + ('*','1'): 'error' + }, + 'x_first': { + ('0','0'): 'x_first', + ('0','1'): 'x_first_accept', + ('1','0'): 'error', + ('1','1'): 'error', + ('*','*'): 'error', + ('0','*'): 'error', + ('*','0'): 'x_first', + ('1','*'): 'error', + ('*','1'): 'x_first_accept' + }, + 'x_first_accept': { + ('*','*'): 'x_first_accept', + ('0','0'): 'error', + ('0','1'): 'error', + ('1','0'): 'error', + ('1','1'): 'error', + ('*','0'): 'error', + ('*','1'): 'error', + ('0','*'): 'error', + ('1','*'): 'error' + }, + 'error': {k: 'error' for k in it.product(base_alphabet, repeat=2)} + }, + initial_state='init', + final_states={'x_first_accept'} # Only when first singleton < second + ) + + # Create the presentation with base automata + presentation = AutomaticPresentation({ + 'U': universe, + 'Subset': subset, + 'Sing': sing, + 'Succ': succ, + 'Lt_sing': lt_sing + }) + + # Define additional relations using formulas + presentation.update( + In="Sing(x) and Subset(x, y)", + Eq_set="Subset(x, y) and Subset(y, x)", + Leq_sing="Lt_sing(x, y) or (Eq_set(x, y) and Sing(x) and Sing(y))", + Gt_sing="not Leq_sing(x, y) and Sing(x) and Sing(y)", + Min="(forall z. not Subset(z, x)) or " # Empty set case + "(Sing(y) and Subset(y, x) and forall z. (-(Sing(z) and Subset(z, x)) or Leq_sing(y, z)))", + Max="Sing(y) and Subset(y, x) and forall z. (-(Sing(z) and Subset(z, x)) or Leq_sing(z, y))", + Intersect="forall a. (-Sing(a) or ((Subset(a, z) and (Subset(a, x) and Subset(a, y))) or (-Subset(a, z) and -(Subset(a, x) and Subset(a, y)))))", + Union="forall a. (-Sing(a) or ((Subset(a, z) and (Subset(a, x) or Subset(a, y))) or (-Subset(a, z) and -(Subset(a, x) or Subset(a, y)))))", + SetMinus="forall a. (-Sing(a) or ((Subset(a, z) and (Subset(a, x) and not Subset(a, y))) or (-Subset(a, z) and -(Subset(a, x) and not Subset(a, y)))))" + ) + + presentation.update( + Geq_sing="not Lt_sing(x, y) and Sing(x) and Sing(y)", + ) + + return presentation + + + + +# -------------------------------------------------------------------------- +# The presentation. It declares its own vocabulary, so `symbolic()` takes no +# argument; see `CompiledPresentation`. +# -------------------------------------------------------------------------- + +class MSO0(CompiledPresentation): + """The finite subsets of :math:`\\mathbb{N}` under :math:`\\subseteq`, with + singletons, successor and the order on singletons. + + >>> M = MSO0() + >>> x, y = M.symbolic().vars("x y") + >>> ({0, 2} , {0, 1, 2}) in x.subset(y) + True + >>> (x + y).eq({0, 1}).check() # union + True + + By Büchi's theorem, first-order logic over this structure is exactly + monadic second-order logic over :math:`(\\mathbb{N}, <)`, so the definable + sets are precisely the regular ones. + """ + + _BUILD = staticmethod(_build_finite_powerset) + + #: a set as a bitmask, position i set iff i is a member. The universe + #: rejects trailing zeros, so the encoding is the CANONICAL one: {0} is + #: `1`, {0, 2} is `101`, and the empty set is the empty word. + PADDING = '*' + + @staticmethod + def encode(s) -> List[str]: + """The word encoding a finite set of naturals: position `i` carries + ``1`` iff `i` is a member, up to the largest one.""" + s = set(s) + if not s: + return [] + if min(s) < 0: + raise ValueError(f"not a set of naturals: {s}") + return ['1' if i in s else '0' for i in range(max(s) + 1)] + + @staticmethod + def decode(word) -> set: + """The set encoded by a word, ignoring padding.""" + digits = ''.join(word).replace(MSO0.PADDING, '') + return {i for i, c in enumerate(digits) if c == '1'} + + def default_signature(self): + """Union as ``+``, intersection as ``*``, difference as binary ``-``, + and the relations of the structure as methods, with sets written as + Python sets.""" + from autstr.symbolic import FunctionCodec, Signature + signature = Signature(codec=FunctionCodec(self.encode, self.decode)) + signature.function('union', graph='Union', out=2) + signature.function('intersect', graph='Intersect', out=2) + signature.function('minus', graph='SetMinus', out=2) + signature.operator('+', 'union') + signature.operator('*', 'intersect') + signature.operator('-', 'minus') + signature.operator('eq', 'Eq_set') + signature.operator('subset', 'Subset') + signature.operator('sing', 'Sing') + # In(x, y): x is a singleton contained in y -- membership, for the + # singletons that stand in for the elements of N. + signature.operator('member_of', 'In') + signature.operator('lt_sing', 'Lt_sing') + return signature diff --git a/autstr/presentations.py b/autstr/presentations.py index f48cbb8..c0fe5e5 100644 --- a/autstr/presentations.py +++ b/autstr/presentations.py @@ -3,7 +3,7 @@ from autstr.sparse_automata import SparseDFA, SparseDFASerializer from autstr.utils.automata_tools import pad, unpad, projection, expand, stack -from autstr.buildin.automata import zero, one +from autstr.utils.automata_tools import zero, one from autstr.utils.logic import get_free_elementary_vars, optimize_query import json @@ -105,10 +105,14 @@ def _parse_payload(cls, payload: bytes): dfa_bytes = bytes(dfa_bytes_list) automata[name] = SparseDFASerializer.from_bytes(dfa_bytes) - # Reconstruct presentation + # Reconstruct presentation. Over a product alphabet the padding symbol + # is a tuple, and JSON has no tuples, so it comes back as a list. + padding_symbol = metadata["padding_symbol"] + if isinstance(padding_symbol, list): + padding_symbol = tuple(padding_symbol) return AutomaticPresentation( automata, - padding_symbol=metadata["padding_symbol"], + padding_symbol=padding_symbol, enforce_consistency=False ) @@ -498,4 +502,25 @@ def _build_automaton(self, phi: logic.Expression, verbose=False, init=True) -> S print(f'{str(phi)}: {result.num_states} states') return result - raise ValueError(f"Unsupported expression type: {type(phi)}") \ No newline at end of file + raise ValueError(f"Unsupported expression type: {type(phi)}") + + +class CompiledPresentation(AutomaticPresentation): + """A presentation whose automata are compiled by a builder function. + + Subclasses set `_BUILD` to that function and declare their vocabulary in + `default_signature`, so the structure can be constructed with no arguments + and addressed symbolically with no setup. The builder's automata are + adopted as they are rather than passed to `AutomaticPresentation.__init__`, + which would restrict and pad relations the builder already restricted and + padded. + """ + + #: the builder, as a staticmethod on the subclass + _BUILD = None + + def __init__(self) -> None: + built = type(self)._BUILD() + self.padding_symbol = built.padding_symbol + self.automata = built.automata + self.sigma = built.sigma diff --git a/autstr/sparse_automata.py b/autstr/sparse_automata.py index 3cf8a94..6636780 100644 --- a/autstr/sparse_automata.py +++ b/autstr/sparse_automata.py @@ -32,7 +32,9 @@ def step(states, symbols): from autstr.mtbdd import ( NONE, STORE, TOP, ComputedTable, NodeStore, bits_of, num_bits, var_tables, ) -from autstr.utils.misc import decode_symbol, encode_symbol +from autstr.utils.misc import ( + alphabet_from_json, decode_symbol, encode_symbol, +) @@ -132,7 +134,7 @@ def _parse_payload(cls, payload: bytes, version: int = None) -> 'SparseDFA': num_states, num_nodes, start_state, symbol_arity, alphabet_len = \ struct.unpack(cls.METADATA_FORMAT, payload[:cls.METADATA_SIZE]) offset = cls.METADATA_SIZE - base_alphabet = set(json.loads(payload[offset:offset + alphabet_len])) + base_alphabet = alphabet_from_json(payload[offset:offset + alphabet_len]) offset += alphabet_len is_accepting = np.frombuffer(payload, dtype=np.uint8, count=num_states, @@ -157,7 +159,7 @@ def _parse_payload_v2(cls, payload: bytes) -> 'SparseDFA': num_states, max_exceptions, start_state, symbol_arity, alphabet_len = \ struct.unpack(cls.METADATA_FORMAT, payload[:cls.METADATA_SIZE]) offset = cls.METADATA_SIZE - base_alphabet = set(json.loads(payload[offset:offset + alphabet_len])) + base_alphabet = alphabet_from_json(payload[offset:offset + alphabet_len]) offset += alphabet_len defaults = np.frombuffer(payload, dtype=np.uint32, count=num_states, diff --git a/autstr/sparse_tree_automata.py b/autstr/sparse_tree_automata.py index 3a1c4a9..929d9d8 100644 --- a/autstr/sparse_tree_automata.py +++ b/autstr/sparse_tree_automata.py @@ -20,13 +20,16 @@ acceptance and touches no diagram at all, and hash-consing makes two states with the same transition function share one node. """ +import json +import struct +import zlib from collections import defaultdict, deque from typing import Dict, List, Optional, Sequence, Set, Tuple import numpy as np from autstr.mtbdd import NONE, STORE, num_bits, var_tables -from autstr.utils.misc import encode_symbol +from autstr.utils.misc import alphabet_from_json, encode_symbol # ==================================================================== @@ -615,3 +618,124 @@ def __repr__(self): return (f"SparseTreeAutomaton({self.num_states} states, " f"{len(self.pair_keys)} pairs, {self.num_nodes} nodes, " f"default={self.default_state})") + + +# ==================================================================== +# Serialization +# ==================================================================== +# +# [Header] magic 'STAU', version, reserved, CRC32 of payload, payload size +# [Payload] metadata (24 bytes), base alphabet (JSON), acceptance array, +# the packed pair keys, then the shared sub-DAG of the transition +# diagrams: var / lo / hi / term arrays and one root per pair. +# +# The diagrams are what makes this worth storing: a relation over a +# convolution alphabet too wide to enumerate still writes out in the size of +# its decision diagrams, exactly as on the string side. + +class SparseTreeAutomatonSerializer: + """Binary serialization for `SparseTreeAutomaton`. + + The tree counterpart of `autstr.sparse_automata.SparseDFASerializer`, and + the same payload idea: the compiled form is a sorted table of child pairs + with one diagram root each, so storing it is storing the pair keys plus + the sub-DAG below their roots. + """ + + MAGIC = b'STAU' + VERSION = 1 + HEADER_FORMAT = "4sB3sII" + HEADER_SIZE = struct.calcsize(HEADER_FORMAT) + #: num_states, num_nodes, num_pairs, default_state, symbol_arity, alphabet + METADATA_FORMAT = "IIIIII" + METADATA_SIZE = struct.calcsize(METADATA_FORMAT) + + @classmethod + def serialize(cls, automaton: 'SparseTreeAutomaton', filename: str) -> None: + with open(filename, 'wb') as handle: + handle.write(cls.to_bytes(automaton)) + + @classmethod + def deserialize(cls, filename: str) -> 'SparseTreeAutomaton': + with open(filename, 'rb') as handle: + return cls.from_bytes(handle.read()) + + @classmethod + def to_bytes(cls, automaton: 'SparseTreeAutomaton') -> bytes: + payload = cls._create_payload(automaton) + header = struct.pack(cls.HEADER_FORMAT, cls.MAGIC, cls.VERSION, + b'\0\0\0', zlib.crc32(payload), len(payload)) + return header + payload + + @classmethod + def from_bytes(cls, data: bytes) -> 'SparseTreeAutomaton': + if len(data) < cls.HEADER_SIZE: + raise ValueError("Data too short for header") + magic, version, _, checksum, payload_size = struct.unpack( + cls.HEADER_FORMAT, data[:cls.HEADER_SIZE]) + if magic != cls.MAGIC: + raise ValueError("Invalid SparseTreeAutomaton format") + if version != cls.VERSION: + raise ValueError( + f"Unsupported SparseTreeAutomaton version: {version}") + payload = data[cls.HEADER_SIZE:cls.HEADER_SIZE + payload_size] + if len(payload) != payload_size: + raise ValueError("Payload size mismatch") + if zlib.crc32(payload) != checksum: + raise ValueError("SparseTreeAutomaton data corruption detected") + return cls._parse_payload(payload) + + @classmethod + def _create_payload(cls, automaton: 'SparseTreeAutomaton') -> bytes: + var, lo, hi, term, roots = STORE.export(automaton.pair_nodes.tolist()) + alphabet_json = json.dumps( + sorted(automaton.base_alphabet_frozen)).encode('utf-8') + metadata = struct.pack( + cls.METADATA_FORMAT, + automaton.num_states, + len(var), + len(automaton.pair_keys), + automaton.default_state, + automaton.symbol_arity, + len(alphabet_json), + ) + return b''.join([ + metadata, + alphabet_json, + np.asarray(automaton.is_accepting, dtype=np.uint8).tobytes(), + np.asarray(automaton.pair_keys, dtype=np.int64).tobytes(), + var.astype(np.int64).tobytes(), + lo.astype(np.int64).tobytes(), + hi.astype(np.int64).tobytes(), + term.astype(np.int64).tobytes(), + np.asarray(roots, dtype=np.int64).tobytes(), + ]) + + @classmethod + def _parse_payload(cls, payload: bytes) -> 'SparseTreeAutomaton': + (num_states, num_nodes, num_pairs, default_state, symbol_arity, + alphabet_len) = struct.unpack(cls.METADATA_FORMAT, + payload[:cls.METADATA_SIZE]) + offset = cls.METADATA_SIZE + base_alphabet = alphabet_from_json(payload[offset:offset + alphabet_len]) + offset += alphabet_len + + is_accepting = np.frombuffer(payload, dtype=np.uint8, count=num_states, + offset=offset).astype(bool) + offset += num_states + + arrays = [] + for count in (num_pairs, num_nodes, num_nodes, num_nodes, num_nodes, + num_pairs): + arrays.append(np.frombuffer(payload, dtype=np.int64, count=count, + offset=offset)) + offset += count * 8 + pair_keys, var, lo, hi, term, roots = arrays + + return SparseTreeAutomaton( + num_states, default_state, + is_accepting=is_accepting, + symbol_arity=symbol_arity, + base_alphabet=base_alphabet, + pair_keys=pair_keys, + pair_nodes=STORE.import_nodes(var, lo, hi, term, roots)) diff --git a/autstr/symbolic/backends.py b/autstr/symbolic/backends.py index 5ce4185..58dab12 100644 --- a/autstr/symbolic/backends.py +++ b/autstr/symbolic/backends.py @@ -9,7 +9,7 @@ from typing import Dict, List, Optional, Sequence -from autstr.buildin.automata import k_longer_automaton +from autstr.utils.automata_tools import k_longer_automaton from autstr.sparse_tree_automata import Tree, convolve_trees, tree_to_arrays from autstr.utils.tree_automata_tools import ( canonical as tree_canonical, iterate_trees, k_deeper_automaton, diff --git a/autstr/tree_algebra.py b/autstr/tree_algebra.py index 5eb152a..cea2ed4 100644 --- a/autstr/tree_algebra.py +++ b/autstr/tree_algebra.py @@ -106,7 +106,7 @@ def default_signature(self): The lattice operations are terms, not connectives: ``&``, ``|`` and ``~`` already mean conjunction, disjunction and negation of *formulas*, so binding them here would make ``x & y`` ambiguous — the same reason - `autstr.arithmetic` spells its divisibility relation + Büchi arithmetic spells its divisibility relation ``divided_by_power``. """ signature = Signature(codec=FunctionCodec(self.encode, self.decode)) diff --git a/autstr/buildin/tree_presentations.py b/autstr/tree_arithmetic.py similarity index 91% rename from autstr/buildin/tree_presentations.py rename to autstr/tree_arithmetic.py index ca264a9..385f191 100644 --- a/autstr/buildin/tree_presentations.py +++ b/autstr/tree_arithmetic.py @@ -1,10 +1,19 @@ -"""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. +"""Skolem arithmetic: the multiplicative monoid of the naturals. + +:math:`(\\mathbb{N}_{>0}, \\cdot)` is *not* string-automatic, but it is +tree-automatic, and the prime factorization is why: multiplicatively the +structure is the direct sum of countably many copies of :math:`(\\mathbb{N}, ++)`, one per prime, and a tree bundles the finitely many nonzero summands. So +multiplication becomes addition of exponents, carried out in parallel across +the primes. + + >>> S = skolem_arithmetic().symbolic() + >>> x, y = S.vars("x y") + >>> (6, 35, 210) in (x * y).eq(S.vars("z")[0]) + True + +This is the tree-engine counterpart of `autstr.arithmetic`, whose additive +structures the string engine can present directly. """ from itertools import product as iter_product from typing import List, Optional diff --git a/autstr/tree_presentations.py b/autstr/tree_presentations.py index c4100cb..e89fe3a 100644 --- a/autstr/tree_presentations.py +++ b/autstr/tree_presentations.py @@ -11,12 +11,17 @@ `project` — which produces the canonical (trimmed) language — is followed by re-saturation, the tree analog of the string pipeline's pad/unpad dance. """ +import json +import struct +import zlib from typing import Dict, Optional, Union from nltk.sem import logic from autstr.presentations import DeferredRelations -from autstr.sparse_tree_automata import SparseTreeAutomaton +from autstr.sparse_tree_automata import ( + SparseTreeAutomaton, SparseTreeAutomatonSerializer, +) from autstr.utils.logic import get_free_elementary_vars, optimize_query from autstr.utils.tree_automata_tools import ( attach_padding, expand, minimize, project, @@ -35,6 +40,87 @@ def tree_zero(symbol_arity: int = 1, base_alphabet=None) -> SparseTreeAutomaton: symbol_arity, base_alphabet or {0}) +class TreeAutomaticPresentationSerializer: + """Binary serialization for `TreeAutomaticPresentation`. + + Mirrors `autstr.presentations.AutomaticPresentationSerializer`, but stores + each automaton's payload as raw bytes with a length prefix rather than as + a JSON list of integers -- which costs roughly four bytes of file per byte + of data. + """ + + MAGIC = b'TPRS' + VERSION = 1 + HEADER_FORMAT = "4sB3sII" + HEADER_SIZE = struct.calcsize(HEADER_FORMAT) + + @classmethod + def serialize(cls, presentation, filename: str) -> None: + payload = cls._create_payload(presentation) + header = struct.pack(cls.HEADER_FORMAT, cls.MAGIC, cls.VERSION, + b'\0\0\0', zlib.crc32(payload), len(payload)) + with open(filename, 'wb') as handle: + handle.write(header) + handle.write(payload) + + @classmethod + def deserialize(cls, filename: str) -> 'TreeAutomaticPresentation': + with open(filename, 'rb') as handle: + data = handle.read() + magic, version, _, checksum, payload_size = struct.unpack( + cls.HEADER_FORMAT, data[:cls.HEADER_SIZE]) + if magic != cls.MAGIC: + raise ValueError("Invalid file format (bad magic number)") + if version != cls.VERSION: + raise ValueError(f"Unsupported version: {version}") + payload = data[cls.HEADER_SIZE:cls.HEADER_SIZE + payload_size] + if len(payload) != payload_size: + raise ValueError("Payload size mismatch") + if zlib.crc32(payload) != checksum: + raise ValueError("Data corruption detected (checksum mismatch)") + return cls._parse_payload(payload) + + @classmethod + def _create_payload(cls, presentation) -> bytes: + names = list(presentation.automata) + metadata = json.dumps({ + "padding_symbol": presentation.padding_symbol, + "max_states": presentation.max_states, + "names": names, + }).encode('utf-8') + chunks = [struct.pack("I", len(metadata)), metadata] + for name in names: + blob = SparseTreeAutomatonSerializer.to_bytes( + presentation.automata[name]) + chunks.append(struct.pack("I", len(blob))) + chunks.append(blob) + return b''.join(chunks) + + @classmethod + def _parse_payload(cls, payload: bytes) -> 'TreeAutomaticPresentation': + metadata_len, = struct.unpack("I", payload[:4]) + offset = 4 + metadata = json.loads(payload[offset:offset + metadata_len]) + offset += metadata_len + + automata = {} + for name in metadata["names"]: + size, = struct.unpack("I", payload[offset:offset + 4]) + offset += 4 + automata[name] = SparseTreeAutomatonSerializer.from_bytes( + payload[offset:offset + size]) + offset += size + + # over a product alphabet the padding symbol is a tuple, and JSON has + # no tuples + padding_symbol = metadata["padding_symbol"] + if isinstance(padding_symbol, list): + padding_symbol = tuple(padding_symbol) + return TreeAutomaticPresentation( + automata, padding_symbol=padding_symbol, + enforce_consistency=False, max_states=metadata["max_states"]) + + class TreeAutomaticPresentation(DeferredRelations): """A presentation of a structure by tree automata. @@ -82,6 +168,21 @@ def _domain_product(self, arity: int) -> SparseTreeAutomaton: minimize(expand(self.automata['U'], arity, [i])))) return domain + def automatic_presentation_to_file(self, filename: str) -> None: + """Write the presentation -- domain, every built relation, alphabet -- + to a file. Deferred relations that have not been built are not stored; + call `materialize` first to include them.""" + TreeAutomaticPresentationSerializer.serialize(self, filename) + + @classmethod + def automatic_presentation_from_file(cls, filename: str): + """Read a presentation written by `automatic_presentation_to_file`. + + The signature is not stored -- a codec is Python code, not data -- so + the result is a bare structure until `symbolic` is given one. + """ + return TreeAutomaticPresentationSerializer.deserialize(filename) + def _install_relation(self, name, definition): self.update(**{name: definition() if callable(definition) else definition}) diff --git a/autstr/uniform.py b/autstr/uniform.py index 8eb2e22..c34fbbc 100644 --- a/autstr/uniform.py +++ b/autstr/uniform.py @@ -19,8 +19,9 @@ from autstr.presentations import AutomaticPresentation, DeferredRelations from autstr.sparse_automata import SparseDFA -from autstr.buildin.automata import one -from autstr.buildin.presentations import create_sparse_dfa, encode_symbol +from autstr.utils.automata_tools import one +from autstr.utils.automata_tools import create_sparse_dfa +from autstr.utils.misc import encode_symbol from autstr.utils.automata_tools import expand, pad, permute_tapes, projection, word_automaton from autstr.utils.logic import get_free_elementary_vars from autstr.utils.misc import get_unique_id diff --git a/autstr/utils/automata_tools.py b/autstr/utils/automata_tools.py index 1882435..f80ecf7 100644 --- a/autstr/utils/automata_tools.py +++ b/autstr/utils/automata_tools.py @@ -1,14 +1,13 @@ import heapq import numpy as np from collections import deque -from typing import Callable, Dict, Generator, List, Set +from typing import Callable, Dict, Generator, List, Optional, Set, Tuple import itertools as it from autstr.mtbdd import NONE, var_tables from autstr.sparse_automata import ( SparseDFA, SparseNFA, _determinize_set_nfa, reduce_set_nfa, ) -from autstr.buildin.automata import one from autstr.utils.misc import decode_symbol, encode_symbol, complement @@ -539,15 +538,19 @@ def iterate_language(dfa: SparseDFA, decoder: Callable = None, heap = LengthLexHeap() for state in start_set: if state in nonempty: - # Represent words as tuple of empty strings - heap.push((tuple(["" for _ in range(arity)]), state)) - + # One tape per argument, each a tuple of letters. Letters are + # kept as they are rather than concatenated into a string: an + # interpreted structure's alphabet is a product alphabet, whose + # letters are themselves tuples, and str() would flatten them + # into unparseable text. + heap.push((tuple([() for _ in range(arity)]), state)) + def cat(word, symbol): - """Concatenate symbol to word based on direction.""" + """Extend a tape by one letter, on the side we are building from.""" if backward: - return str(symbol) + word + return (symbol,) + word else: - return word + str(symbol) + return word + (symbol,) def push(heap, word_tuple, sym_enc, next_state): """Push a new word onto the heap with the given extension symbol and next state.""" @@ -801,3 +804,209 @@ def partial_dfa(base_alphabet: Set, arity: int, symbol_arity=arity, base_alphabet=set(base_alphabet), ).minimize() + + +# -------------------------------------------------------------------------- +# Basic automata the constructions above build on: fixed and relative word +# lengths, and the two constant languages. +# -------------------------------------------------------------------------- + +def length_automaton(n: int, base_alphabet: Set[int]) -> SparseDFA: + """ + Creates an automaton that recognizes all words over base_alphabet with length exactly n. + + :param n: The exact word length + :param base_alphabet: Set of integer symbols + :return: SparseDFA recognizing words of length n + """ + # States: 0 (start), 1, 2, ..., n (accepting), n+1 (dead) + num_states = n + 2 + # Default transitions: move to next state or dead state + default_states = np.array([i + 1 for i in range(n)] + [n + 1, n + 1], dtype=np.int32) + # No exceptions needed (same behavior for all symbols) + exception_symbols = np.full((num_states, 0), -1, dtype=np.int32) + exception_states = np.full((num_states, 0), -1, dtype=np.int32) + # Only state n is accepting + is_accepting = np.array([False] * n + [True, False]) + start_state = 0 + + return SparseDFA( + num_states=num_states, + default_states=default_states, + exception_symbols=exception_symbols, + exception_states=exception_states, + is_accepting=is_accepting, + start_state=start_state, + symbol_arity=1, + base_alphabet=base_alphabet + ) + +def k_longer_automaton(k: int, r: int, base_alphabet: Set[int], padding_symbol: int) -> SparseDFA: + """ + Creates an automaton recognizing (r+1)-tuples where the last word is at least k letters + longer than the other r words. + + :param k: Minimal length difference + :param r: Number of reference words + :param base_alphabet: Set of integer symbols + :param padding_symbol: Padding symbol integer + :return: SparseDFA for the k-longer condition + """ + # State mapping: [-1, 0, 1, ..., k] -> [0, 1, 2, ..., k+1] + state_mapping = {s: i for i, s in enumerate(range(-1, k+1))} + num_states = len(state_mapping) + sorted_alphabet = sorted(base_alphabet) + arity = r + 1 + + # Precompute all symbol tuples and their encodings + symbol_tuples = list(it.product(sorted_alphabet, repeat=arity)) + symbol_encodings = [encode_symbol(t, base_alphabet) for t in symbol_tuples] + + # Initialize DFA components + default_states = np.full(num_states, state_mapping[-1], dtype=np.int32) # Default to dead state + exception_list = [[] for _ in range(num_states)] + + # Build transitions + for state in range(-1, k+1): + state_idx = state_mapping[state] + for t, enc in zip(symbol_tuples, symbol_encodings): + # Compute next state + if state == -1: + next_state = -1 # Stay in dead state + else: + if all(x == padding_symbol for x in t[:-1]) and t[-1] != padding_symbol: + next_state = min(state + 1, k) # Count extra length + elif t[-1] == padding_symbol: + next_state = -1 # Reject if padding the last word + elif state == 0: + next_state = 0 # Wait for other words to end + else: + next_state = -1 # Reject otherwise + + next_state_idx = state_mapping[next_state] + if next_state_idx != state_mapping[-1]: + exception_list[state_idx].append((enc, next_state_idx)) + + # Find max exceptions needed + max_exceptions = max(len(ex_list) for ex_list in exception_list) if exception_list else 0 + + # Build exception arrays + exception_symbols = np.full((num_states, max_exceptions), -1, dtype=np.int32) + exception_states = np.full((num_states, max_exceptions), -1, dtype=np.int32) + + for i, ex_list in enumerate(exception_list): + if ex_list: + syms, states = zip(*ex_list) + exception_symbols[i, :len(syms)] = syms + exception_states[i, :len(states)] = states + + # Final states: state k (meaning we've counted k extra symbols) + is_accepting = np.array([i == state_mapping[k] for i in range(num_states)]) + + return SparseDFA( + num_states=num_states, + default_states=default_states, + exception_symbols=exception_symbols, + exception_states=exception_states, + is_accepting=is_accepting, + start_state=state_mapping[0], + symbol_arity=arity, + base_alphabet=base_alphabet + ) + + +def zero(symbol_arity: int = 1, base_alphabet: Optional[Set[int]] = None) -> SparseDFA: + """Automaton that rejects all inputs.""" + base_alphabet = base_alphabet or {0} + return SparseDFA( + num_states=1, + default_states=np.array([0], dtype=np.int32), + exception_symbols=np.full((1, 0), -1, dtype=np.int32), + exception_states=np.full((1, 0), -1, dtype=np.int32), + is_accepting=np.array([False]), + start_state=0, + symbol_arity=symbol_arity, + base_alphabet=base_alphabet + ) + +def one(symbol_arity: int = 1, base_alphabet: Optional[Set[int]] = None) -> SparseDFA: + """Automaton that accepts all inputs.""" + base_alphabet = base_alphabet or {0} + return SparseDFA( + num_states=1, + default_states=np.array([0], dtype=np.int32), + exception_symbols=np.full((1, 0), -1, dtype=np.int32), + exception_states=np.full((1, 0), -1, dtype=np.int32), + is_accepting=np.array([True]), + start_state=0, + symbol_arity=symbol_arity, + base_alphabet=base_alphabet + ) + + +def create_sparse_dfa(states: List[str], input_symbols: Set[Tuple[str]], + transitions: Dict[str, Dict[Tuple[str], str]], + initial_state: str, final_states: Set[str]) -> SparseDFA: + """Convert a traditional DFA description to a SparseDFA.""" + # Map states to integers + state_to_index = {s: i for i, s in enumerate(states)} + num_states = len(states) + + # Determine base alphabet and arity + base_alphabet = set() + for sym in input_symbols: + for char in sym: + base_alphabet.add(char) + arity = len(next(iter(input_symbols))) if input_symbols else 0 + + # Create state arrays + default_states = [] + exception_symbols = [] + exception_states = [] + is_accepting = np.array([state in final_states for state in states], dtype=bool) + + # Build symbol mapping + symbol_map = {} + for symbol in input_symbols: + symbol_map[symbol] = encode_symbol(symbol, frozenset(base_alphabet)) + + # Process each state + for state in states: + # Find most common transition + next_states = [transitions[state][sym] for sym in input_symbols] + default_target = max(set(next_states), key=next_states.count) + default_states.append(state_to_index[default_target]) + + # Collect exceptions + exceptions = [] + for symbol, next_state in transitions[state].items(): + if next_state != default_target: + sym_enc = symbol_map[symbol] + next_idx = state_to_index[next_state] + exceptions.append((sym_enc, next_idx)) + + # Sort exceptions by symbol for consistency + exceptions.sort(key=lambda x: x[0]) + exception_symbols.append([e[0] for e in exceptions]) + exception_states.append([e[1] for e in exceptions]) + + # Pad exceptions + max_exceptions = max(len(e) for e in exception_symbols) if exception_symbols else 0 + padded_ex_syms = np.full((num_states, max_exceptions), -1, dtype=np.int32) + padded_ex_states = np.full((num_states, max_exceptions), -1, dtype=np.int32) + + for i in range(num_states): + if exception_symbols[i]: + padded_ex_syms[i, :len(exception_symbols[i])] = exception_symbols[i] + padded_ex_states[i, :len(exception_states[i])] = exception_states[i] + + return SparseDFA( + num_states=num_states, + default_states=np.array(default_states, dtype=np.int32), + exception_symbols=padded_ex_syms, + exception_states=padded_ex_states, + is_accepting=is_accepting, + start_state=state_to_index[initial_state], + symbol_arity=arity, + base_alphabet=base_alphabet + ).minimize() diff --git a/autstr/utils/misc.py b/autstr/utils/misc.py index a8577cd..37d515a 100644 --- a/autstr/utils/misc.py +++ b/autstr/utils/misc.py @@ -1,3 +1,4 @@ +import json from functools import cmp_to_key from heapq import heapify, heappop, heappush from typing import FrozenSet, Set, List, Tuple, Union @@ -113,4 +114,15 @@ def complement(values, min_val: int, max_val: int) -> np.ndarray: values = np.asarray(values) if values.size == 0: return np.array([], dtype=values.dtype) - return np.setdiff1d(np.arange(min_val, max_val + 1), values) \ No newline at end of file + return np.setdiff1d(np.arange(min_val, max_val + 1), values) + + +def alphabet_from_json(raw) -> set: + """The base alphabet as stored in a serialized payload. + + JSON has no tuples, so a product alphabet's letters -- which is what an + interpreted structure of dimension > 1 has -- come back as lists. Restore + them, or the set() built from them raises on the first unhashable letter. + """ + return {tuple(letter) if isinstance(letter, list) else letter + for letter in json.loads(raw)} diff --git a/autstr/utils/tree_automata_tools.py b/autstr/utils/tree_automata_tools.py index 21b7523..3971758 100644 --- a/autstr/utils/tree_automata_tools.py +++ b/autstr/utils/tree_automata_tools.py @@ -532,7 +532,7 @@ def k_deeper_automaton(k: int, references: int, base_alphabet, reference tape: some root-to-leaf path carries `k` nodes at which all `references` reference tapes are padding and the last tape is not. - The tree counterpart of `buildin.automata.k_longer_automaton`, and it + The tree counterpart of `automata_tools.k_longer_automaton`, and it supports exists-infinity for the same pumping reason. A tree's domain is closed under parents, so the nodes outside every reference's domain form a suffix of each root-to-leaf path; `k` of them make a body automaton with diff --git a/docs/media/history.gif b/docs/media/history.gif index 8fb7f47..1803b84 100644 --- a/docs/media/history.gif +++ b/docs/media/history.gif @@ -1,3 +1,3 @@ version https://git-lfs.github.com/spec/v1 -oid sha256:e059a611435f7f5fc6b8705ad9d8c360ab217e8e1bb7ff6f4147cacd307f017d -size 2418080 +oid sha256:f1d687abb50e728c2c957280a88847079bbfd731df6d09e4d11e0c07572fcb3e +size 2831196 diff --git a/docs/source/conf.py b/docs/source/conf.py index 0d0e027..bcdbe02 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -59,6 +59,10 @@ for _img in sorted((_here.parent / 'media').glob('*.png')): shutil.copyfile(_img, _media_dst / _img.name) +# Copy the changelog into the source tree so it has a page of its own; it +# lives at the repository root, where GitHub and PyPI look for it. +shutil.copyfile(_here.parent.parent / 'CHANGELOG.md', _here / 'changelog.md') + nb_execution_mode = 'force' nb_execution_timeout = 900 nb_execution_raise_on_error = True diff --git a/docs/source/index.rst b/docs/source/index.rst index 522f437..38fbc99 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -18,6 +18,7 @@ reference is generated from the docstrings. :caption: Notebooks notebooks/arithmetic_and_algebra + notebooks/infinite_structures notebooks/graphs notebooks/groups notebooks/composition @@ -29,6 +30,13 @@ reference is generated from the docstrings. api/modules +.. toctree:: + :maxdepth: 1 + :caption: Project + + changelog + references + Indices and tables ================== diff --git a/docs/source/overview.md b/docs/source/overview.md index e01ddf0..43574b7 100644 --- a/docs/source/overview.md +++ b/docs/source/overview.md @@ -17,7 +17,7 @@ An `AutomaticPresentation` bundles automata for a domain and its relations, and decides first-order statements about the presented structure: ```python -from autstr.buildin.presentations import BuechiArithmeticZ +from autstr.arithmetic import BuechiArithmeticZ Z = BuechiArithmeticZ() # (ℤ, +, <, |) as automata @@ -25,8 +25,9 @@ Z.check('all x.(exists y.(A(x,y,x)))') # ∀x ∃y: x+y=x — True Z.check('exists x.(all y.(Lt(x,y)))') # a least integer? — False ``` -Because the first-order theory of an automatic structure is decidable, `check` -always terminates with a definite answer — a theorem prover for the fragment of +Because the first-order theory of an automatic structure is decidable +({ref}`Khoussainov & Nerode `, {ref}`Blumensath & Grädel +`), `check` always terminates with a definite answer — a theorem prover for the fragment of mathematics these structures capture. `evaluate` goes further and returns the automaton of *all* satisfying assignments, which you can enumerate or reuse. The {doc}`arithmetic & algebra notebook ` walks @@ -41,10 +42,10 @@ relation symbols and function symbols that compose with ordinary Python operators. ```python -from autstr.arithmetic import integers +from autstr.arithmetic import BuechiArithmeticZ -Z = integers() -x, y, z = Z.vars('x y z') +Z = BuechiArithmeticZ().symbolic() # no arguments: the structure knows its own +x, y, z = Z.vars('x y z') # vocabulary phi = (x + y).eq(z) & z.lt(100) # a relation over x, y, z phi.check() # satisfiable? — True @@ -61,10 +62,11 @@ restores the names in results. What a structure offers is declared in a `Signature`: which relations are function graphs, which operators they bind to, and how Python values encode as -elements. +elements. Every structure in the library declares its own, which is why +`symbolic()` above needed no argument. For a presentation you built yourself, +write one: ```python -from autstr.arithmetic import encode, decode from autstr.symbolic import Signature, FunctionCodec signature = (Signature(codec=FunctionCodec(encode, decode)) @@ -75,6 +77,11 @@ signature = (Signature(codec=FunctionCodec(encode, decode)) S = my_presentation.symbolic(signature) ``` +`encode` and `decode` are the structure's own — a Python value to the word that +represents it, and back — so results come out as the values you put in. Give a +presentation a `default_signature` method returning this, and its `symbolic()` +takes no argument either. + Results carry their tape order as variable *names*, so membership and enumeration are keyed by name rather than position: @@ -112,9 +119,10 @@ element of ℤ[1/2] is 2-divisible but not 3-divisible, and vice versa for ℤ[1 ## Uniformly automatic classes: one automaton for a whole family -A **uniformly automatic class** presents not one structure but an entire *family*, -by giving every automaton one extra tape that reads an **advice string** -synchronously with the elements. Fixing the advice instantiates one member; a +A **uniformly automatic class** ({ref}`Abu Zaid, Grädel & Reinhardt +`) presents not one structure but an entire *family*, by giving +every automaton one extra tape that reads an **advice string** synchronously +with the elements. Fixing the advice instantiates one member; a query is compiled once for the class and then decides any member by running its advice word through the resulting automaton. @@ -146,10 +154,11 @@ complex relations from primitives. The same machinery runs over **trees** rather than words. Where an automatic presentation encodes elements as strings and a word automaton reads them, a *tree-automatic* presentation encodes them as finite trees read by a bottom-up -tree automaton — exactly the step from Büchi's theorem to Rabin's. +tree automaton — exactly the step from {ref}`Büchi's theorem ` to +{ref}`Rabin's `. `autstr.tree_uniform` hosts the classes whose advice is naturally a tree: a tree decomposition (bounded tree-width) or a k-expression (bounded clique-width), and -Skolem arithmetic (ℕ, ·) in `autstr.buildin.tree_presentations`, where a number +Skolem arithmetic (ℕ, ·) in `autstr.tree_arithmetic`, where a number is the tree of its prime exponents. The {doc}`graphs ` and {doc}`groups ` @@ -215,6 +224,70 @@ cyclic groups, and it predates the module. The {doc}`composition notebook ` walks through all five operations. +## Defining one structure inside another + +Automatic structures are closed under **first-order interpretation**, and +`autstr.interpretations` does not merely record that — it *computes* the +interpreted presentation. You give a domain formula δ(x̄), a formula per +relation, a dimension *k* (an element is a *k*-tuple of source elements), and +optionally a definable equivalence ε whose classes become the elements: + +```python +Z = interpret(BuechiArithmetic(), # the integers from the naturals + domain=('Eq(x0,x0) and Eq(x1,x1)', ['x0', 'x1']), + relations={'Lt': (LESS, pair), 'Eq': (SAME, pair)}, + dimension=2, quotient=(SAME, pair)) +``` + +A quotient needs one representative per class. Over words that is the +shortlex-least member, and shortlex is a well-order, so it exists. Over +**trees** no automatic order is well-founded — growing a tree where two members +differ makes it *smaller* — so a class need have no least member at all, and +the representative is instead the least *description* +({ref}`Kuske & Weidner `; existence is +{ref}`Colcombet & Löding `). That construction is provably +exponential in the worst case, which is why `max_states` is worth passing. + +The **ordinals** are the payoff example. By Cantor normal form an ordinal below +ω^n is an n-tuple of naturals under reverse-lexicographic order, so +`autstr.ordinals` is three formulas over Büchi arithmetic and no automaton +authored by hand. How far this reaches is exactly +{ref}`Delhommé's theorem `: the word-automatic ordinals are those +below ω^ω and the tree-automatic ones those below ω^(ω^ω) — which is why +`Ordinal` and `TreeOrdinal` take an exponent instead of being single +structures. + +## Infinite graphs, and where first-order logic stops + +`autstr.infinite_graphs` presents the Cayley graph of ℤⁿ (an asynchronous +product) and the infinite k-regular tree with its prefix order. +`autstr.turing` presents a Turing machine's **configuration graph**: one step +is a bounded rewrite, so the graph is automatic and its first-order theory is +decidable. What you may not ask is whether one configuration *reaches* another — +that is halting, and no first-order formula over this graph can express it. + +Level 2 **collapsible pushdown systems** are where that changes. Their stacks +are stacks of stacks whose letters carry collapse links, and their configuration +graphs are tree-automatic by {ref}`Kartzow's encoding ` — blocks +hang off each other as a tree and the links are recovered from its shape rather +than stored. MSO over these graphs is undecidable, so this is the only +automatic route to them. + +For these graphs **reachability is a relation like any other**. Every run +decomposes into four stretches — words leaving the stack, letters leaving, +letters returning, words returning — each of them reflexive, so + +``` +Reach(x, y) = ∃d ∃f ∃g. A(x, d) ∧ B(d, f) ∧ C(f, g) ∧ D(g, y) +``` + +is a first-order formula over four automata rather than a fixpoint over trees. +It is exponential in the number of control states, so it is *declared* up front +and built the first time a query mentions it. The +{doc}`infinite structures notebook ` builds one +and decides that its reachability is transitive — a statement about all runs of +all lengths. + ## Bounded rank-width: groups and graphs from one linear algebra The width notions above bound how much *combinatorial* structure crosses a cut. @@ -309,7 +382,7 @@ is **decidable**, and every definable relation is again automatic. ### A concrete encoding -In the arithmetic package an integer is written **sign-magnitude, least-significant +In Büchi arithmetic an integer is written **sign-magnitude, least-significant bit first**: the first symbol is a sign bit (`0` for non-negative, `1` for negative), followed by the binary digits of the magnitude from the lowest bit upward, with `*` padding the shorter arguments of a multi-tape relation so all @@ -351,12 +424,14 @@ exponents, and classes whose advice is inherently a tree. Evaluating a *fixed* formula on a structure is one linear pass of its advice through the query automaton, so on any class of bounded width every fixed MSO property is -decided in linear time — a constructive, streaming form of Courcelle's theorem. The +decided in linear time — a constructive, streaming form of +{ref}`Courcelle's theorem `. The cost lives entirely in *compiling* the automaton. A transition is not a `symbol -> target` table but a **decision diagram over the symbol's digits**, hash-consed and shared across states and automata -(`autstr.mtbdd`) — the representation MONA uses, for the same reason. A transition +(`autstr.mtbdd`) — the representation {doc}`MONA ` uses, for the +same reason. A transition that ignores a tape never tests that tape's variables, so cylindrification is a variable renaming rather than a duplication of every row once per letter of every new tape, complementation touches no diagram at all, and the alphabet's *width* diff --git a/docs/source/references.md b/docs/source/references.md new file mode 100644 index 0000000..ad3e50c --- /dev/null +++ b/docs/source/references.md @@ -0,0 +1,165 @@ +# References + +Every construction in AutStr comes from somewhere. This page collects those +sources and says, for each, what in the library it is. The +{doc}`overview ` links here wherever a named theorem or construction +is used. + +## Foundations + +The idea that a logic can be decided by translating formulas into automata long +predates the term *automatic structure*. + +(buechi1960)= +**Büchi, J. R.** *Weak Second-Order Arithmetic and Finite Automata.* +Zeitschrift für math. Logik und Grundlagen der Mathematik 6 (1960), 66–92. +DOI: [10.1002/malq.19600060105](https://doi.org/10.1002/malq.19600060105) +: Monadic second-order logic over (ℕ, +1) is decidable, by translation into + finite automata. **Every `evaluate` call in this library is this + construction**, and `autstr.powerset.MSO0` is the structure that makes the + correspondence literal: first-order logic over it *is* MSO over (ℕ, <). + +(rabin1969)= +**Rabin, M. O.** *Decidability of Second-Order Theories and Automata on +Infinite Trees.* Transactions of the AMS 141 (1969), 1–35. +DOI: [10.2307/1995086](https://doi.org/10.2307/1995086) +: The same programme over trees. `autstr.sparse_tree_automata` and every + tree-automatic presentation here are the finite-tree fragment of this. + +(courcelle1990)= +**Courcelle, B.** *The Monadic Second-Order Logic of Graphs I: Recognizable +Sets of Finite Graphs.* Information and Computation 85(1), 1990, 12–75. +DOI: [10.1016/0890-5401(90)90043-H](https://doi.org/10.1016/0890-5401%2890%2990043-H) +: MSO properties of graphs of bounded tree-width are decidable in linear time. + `autstr.tree_graphs.TreeWidthClass` builds the automaton the theorem + promises — and, because the class is compiled once and each member is one + linear pass, in a constructive and streaming form. + +(makowsky2004)= +**Makowsky, J. A.** *Algorithmic Uses of the Feferman–Vaught Theorem.* +Annals of Pure and Applied Logic 126 (2004), 159–213. +DOI: [10.1016/j.apal.2003.11.002](https://doi.org/10.1016/j.apal.2003.11.002) +: The composition method behind meta-theorems of this shape, and behind + `autstr.composition`. + +## Automatic structures + +(khoussainov1994)= +**Khoussainov, B., & Nerode, A.** *Automatic presentations of structures.* +LCC 1994, LNCS vol. 960, Springer. +DOI: [10.1007/3-540-60178-3_93](https://doi.org/10.1007/3-540-60178-3_93) +: The definition the whole library implements: a structure presented by + automata for its domain and relations. + +(blumensath2000)= +**Blumensath, A., & Grädel, E.** *Automatic Structures.* LICS 2000, pp. 51–62. +[Proceedings](https://lics.siglog.org/2000/Grdel-AutomaticStructures.html) +: Closure under first-order definability, and hence the decidability that + `check` relies on. `autstr.interpretations` computes the closure under + interpretations that this theory guarantees. + +(khoussainov2007)= +**Khoussainov, B., Rubin, S., & Stephan, F.** *Automatic Structures: Richness +and Limitations.* LMCS 3(2), 2007. +arXiv: [cs/0703064](https://arxiv.org/abs/cs/0703064) · +DOI: [10.2168/LMCS-3(2:2)2007](https://doi.org/10.2168/LMCS-3%282%3A2%292007) +: Where the boundaries are — which structures cannot be automatic, and why + some of the constructions here need the tree engine. + +(delhomme2004)= +**Delhommé, C.** *Automaticité des ordinaux et des graphes homogènes.* +Comptes Rendus Mathématique 339(1), 2004, 5–10. +DOI: [10.1016/j.crma.2004.03.035](https://doi.org/10.1016/j.crma.2004.03.035) +: The two lines `autstr.ordinals` sits between: the word-automatic ordinals are + exactly those below ω^ω, and the tree-automatic ones exactly those below + ω^(ω^ω). `Ordinal(n)` and `TreeOrdinal(n)` take an exponent rather than being + single structures precisely because neither boundary ordinal is reachable. + +(colcombet2007)= +**Colcombet, T., & Löding, C.** *Transforming structures by set +interpretations.* Logical Methods in Computer Science 3(2:4), 2007, 1–36. +DOI: [10.2168/LMCS-3(2:4)2007](https://doi.org/10.2168/LMCS-3%282%3A4%292007) +: Set interpretations, and their application to tree-automatic structures. + Every tree-automatic structure admits an *injective* presentation, which is + what makes `interpret(..., quotient=ε)` well posed over trees; Kuske and + Weidner below make that effective. + +(kuske2011)= +**Kuske, D., & Weidner, T.** *Size and Computation of Injective Tree Automatic +Presentations.* MFCS 2011, LNCS vol. 6907, pp. 424–435. +DOI: [10.1007/978-3-642-22993-0_39](https://doi.org/10.1007/978-3-642-22993-0_39) +: The construction `autstr.interpretations` uses for tree quotients. No + automatic order on trees is well-founded, so a class need have no least + member; the representative is instead the least *description*. §4 proves the + exponential blowup unavoidable, which is why `max_states` is worth passing. + +## Uniformly automatic classes + +(abuzaid2016)= +**Abu Zaid, F.** *Algorithmic Solutions via Model Theoretic Interpretations.* +Dissertation, RWTH Aachen University, 2016. +DOI: [10.18154/RWTH-2017-07663](https://doi.org/10.18154/RWTH-2017-07663) + +(abuzaid2017)= +**Abu Zaid, F., Grädel, E., & Reinhardt, F.** *Advice Automatic Structures and +Uniformly Automatic Classes.* CSL 2017, LIPIcs vol. 82, pp. 35:1–35:20. +DOI: [10.4230/LIPIcs.CSL.2017.35](https://doi.org/10.4230/LIPIcs.CSL.2017.35) +: Introduces automatic presentations with advice — the foundation of + `autstr.uniform` and every class in the library. The ℤ[1/p] presentation in + `autstr.algebra` follows its blueprint for (ℚ, +). + +(abuzaid2018)= +**Abu Zaid, F.** *Uniformly Automatic Classes of Finite Structures.* +FSTTCS 2018, LIPIcs vol. 122, pp. 10:1–10:21. +DOI: [10.4230/LIPIcs.FSTTCS.2018.10](https://doi.org/10.4230/LIPIcs.FSTTCS.2018.10) +: The meta-theorems for finite Boolean algebras, finite groups, and graphs of + bounded tree-depth implemented by `autstr.uniform`, `autstr.graphs`, + `autstr.algebra` and `autstr.groups`. + +## Width parameters + +(courcelle2000)= +**Courcelle, B., & Olariu, S.** *Upper Bounds to the Clique Width of Graphs.* +Discrete Applied Mathematics 101 (2000), 77–114. +DOI: [10.1016/S0166-218X(99)00184-5](https://doi.org/10.1016/S0166-218X%2899%2900184-5) +: The k-expressions that `autstr.tree_graphs.CliqueWidthClass` reads as advice. + +(oum2006)= +**Oum, S., & Seymour, P.** *Approximating clique-width and branch-width.* +Journal of Combinatorial Theory Series B 96(4), 2006, 514–528. +DOI: [10.1016/j.jctb.2005.10.006](https://doi.org/10.1016/j.jctb.2005.10.006) +: The paper that introduces **rank-width**, as the branch-width of the cut-rank + function. Rank decompositions are the advice of + `autstr.tree_graphs.RankWidthClass`, and the width measure the class-2 group + families in `autstr.groups`, `autstr.tree_groups` and + `autstr.cocycle_groups` are graded by. + +## Higher-order pushdown graphs + +(kartzow2013)= +**Kartzow, A.** *Collapsible Pushdown Graphs of Level 2 are Tree-Automatic.* +Logical Methods in Computer Science 9(1:12), 2013. +arXiv: [1303.2453](https://arxiv.org/abs/1303.2453) · +DOI: [10.2168/LMCS-9(1:12)2013](https://doi.org/10.2168/LMCS-9%281%3A12%292013) +: The encoding `autstr.collapsible` implements — blocks as a tree, collapse + links recovered from its shape rather than stored — and the reachability + decomposition `autstr.collapsible_reach` builds: §4 splits every run into + four stretches, §5 turns that into a relation of the graph. Since MSO over + these graphs is undecidable, this is the only automatic route to them. + +## Related tools + +**[MONA](https://www.brics.dk/mona/)** (Klarlund, Møller, Henriksen et al.) +: Decides WS1S and WS2S by translating formulas to automata whose transitions + are shared multi-terminal BDDs over the symbol's bits. + {py:mod}`autstr.mtbdd` adopts exactly that representation, for exactly MONA's + reason: over a convolution alphabet, the flat `symbol -> target` table is the + bottleneck. + +**[Walnut](https://cs.uwaterloo.ca/~shallit/walnut.html)** (Mousavi, Shallit) +: Proves theorems about automatic sequences by deciding first-order statements + over (ℕ, +) with automata — the same decision procedure, aimed at + combinatorics on words rather than at presenting structures. + +Both are mature and fast, and neither targets *uniformly* automatic classes or +arbitrary automatic presentations, which is where AutStr sits. diff --git a/notebooks/arithmetic_and_algebra.ipynb b/notebooks/arithmetic_and_algebra.ipynb index 341fa6f..a824141 100644 --- a/notebooks/arithmetic_and_algebra.ipynb +++ b/notebooks/arithmetic_and_algebra.ipynb @@ -35,9 +35,9 @@ "source": [ "## Presburger arithmetic over the integers\n", "\n", - "$(\\mathbb{Z}, +, <)$ is automatic in base 2. `autstr.arithmetic` exposes it through\n", - "a small term algebra, so an *infinite* definable set is an ordinary Python value you\n", - "can intersect, complement and iterate." + "$(\\mathbb{Z}, +, <)$ is automatic in base 2. Calling `.symbolic()` on the presentation\n", + "hands out variables that compose with Python operators, so an *infinite* definable set\n", + "is an ordinary Python value you can intersect, complement and iterate." ] }, { @@ -47,10 +47,10 @@ "metadata": {}, "outputs": [], "source": [ - "from autstr.arithmetic import integers\n", + "from autstr.arithmetic import BuechiArithmeticZ\n", "from time import time\n", "\n", - "Z = integers()\n", + "Z = BuechiArithmeticZ().symbolic() # the structure declares its own vocabulary\n", "x = Z.var('x')" ] }, @@ -212,7 +212,7 @@ "metadata": {}, "outputs": [], "source": [ - "from autstr.buildin.presentations import BuechiArithmetic\n", + "from autstr.arithmetic import BuechiArithmetic\n", "\n", "ba = BuechiArithmetic()\n", "ba.automata['A'].show_diagram() # the addition relation A(x, y, z): x + y = z" @@ -288,7 +288,7 @@ "metadata": {}, "outputs": [], "source": [ - "from autstr.buildin.tree_presentations import skolem_arithmetic\n", + "from autstr.tree_arithmetic import skolem_arithmetic\n", "\n", "skolem = skolem_arithmetic()\n", "print('360 = 2^3 * 3^2 * 5 round-trips to:', skolem.decode(skolem.encode(360)))\n", @@ -348,6 +348,63 @@ " dfa.accepts([(s,) for s in advice]))" ] }, + { + "cell_type": "markdown", + "id": "77fa08cf", + "metadata": {}, + "source": [ + "## The countable atomless Boolean algebra\n", + "\n", + "Every *finite* Boolean algebra is a powerset, so it is full of **atoms** —\n", + "minimal nonzero elements. Drop finiteness and something else becomes possible: a\n", + "Boolean algebra in which every nonzero element splits, forever. There is exactly\n", + "one countable such algebra up to isomorphism, and it is the clopen algebra of\n", + "Cantor space.\n", + "\n", + "Its elements are *sets of binary strings* — the cylinders a clopen set contains —\n", + "so an element is a finite tree, and the presentation lives on the **tree**\n", + "engine. Meet, join and complement are `*`, `+` and unary `-`; the lattice order\n", + "is `.leq`." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "26a35f81", + "metadata": {}, + "outputs": [], + "source": [ + "from autstr.tree_algebra import AtomlessBooleanAlgebra\n", + "\n", + "B = AtomlessBooleanAlgebra()\n", + "S = B.symbolic()\n", + "x, y, z = S.vars('x y z')\n", + "\n", + "# the cylinder \"strings starting 0\" and its complement partition the space\n", + "print('0 join 1 = everything:', ({'0'}, {'1'}, {''}) in (x + y).eq(z))\n", + "print('complement of 0 is 1: ', ({'0'}, {'1'}) in (-x).eq(y))\n", + "print('00 <= 0: ', ({'00'}, {'0'}) in x.leq(y))" + ] + }, + { + "cell_type": "markdown", + "id": "de601520", + "metadata": {}, + "source": [ + "The defining property is a *sentence*, so it is something to decide rather than\n", + "to assert: every nonzero element strictly contains a nonzero element." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "3e249058", + "metadata": {}, + "outputs": [], + "source": [ + "print('atomless:', B.is_atomless())" + ] + }, { "cell_type": "markdown", "id": "f9cf091f", @@ -415,7 +472,11 @@ "and order on singletons, form the structure MSO0. A finite set is a $\\{0,1\\}$-word\n", "(position $i$ set iff $i$ is a member), and — by Büchi's theorem — first-order logic\n", "over MSO0 is precisely **monadic second-order** logic over $(\\mathbb{N}, <)$: the\n", - "definable sets are exactly the regular ones." + "definable sets are exactly the regular ones.\n", + "\n", + "The encoding is *canonical*: the universe rejects trailing zeros, so $\\{0\\}$ is the\n", + "word `1` and $\\emptyset$ is the empty word. The structure's codec knows this, so\n", + "ordinary Python sets go in and come out." ] }, { @@ -425,7 +486,7 @@ "metadata": {}, "outputs": [], "source": [ - "from autstr.buildin.presentations import MSO0\n", + "from autstr.powerset import MSO0\n", "\n", "mso0 = MSO0()\n", "print('relations:', mso0.get_relation_symbols())\n", @@ -447,6 +508,48 @@ " mso0.check('exists x.(Sing(x) and all y.((not Sing(y)) or Leq_sing(x,y)))'))" ] }, + { + "cell_type": "markdown", + "id": "4fa93591", + "metadata": {}, + "source": [ + "### Sets as Python sets\n", + "\n", + "Symbolically the Boolean operations are the arithmetic ones: union is `+`, intersection\n", + "`*`, and set difference binary `-`. Membership, subset and singleton-hood are methods." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "72e189ba", + "metadata": {}, + "outputs": [], + "source": [ + "S = mso0.symbolic()\n", + "x, y, z = S.vars('x y z')\n", + "\n", + "print('{0,1} u {1,2} = {0,1,2}:', ({0, 1}, {1, 2}, {0, 1, 2}) in (x + y).eq(z))\n", + "print('{0,1} n {1,2} = {1}: ', ({0, 1}, {1, 2}, {1}) in (x * y).eq(z))\n", + "print('{0,1} \\\\ {1,2} = {0}: ', ({0, 1}, {1, 2}, {0}) in (x - y).eq(z))\n", + "print('{0,2} subset {0,1,2}: ', ({0, 2}, {0, 1, 2}) in x.subset(y))\n", + "\n", + "# Solutions come back as sets: the ways to split {0,1,2} into two disjoint pieces.\n", + "disjoint_cover = (x + y).eq({0, 1, 2}) & (x * y).eq(set())\n", + "for a, b in sorted(disjoint_cover, key=lambda p: (len(p[0]), sorted(p[0]))):\n", + " print(f' {a or set()} + {b or set()}')" + ] + }, + { + "cell_type": "markdown", + "id": "e25efbf0", + "metadata": {}, + "source": [ + "Each of those is a first-order query over MSO0, which is to say a **monadic\n", + "second-order** query over $(\\mathbb{N}, <)$ — quantifying over sets here costs no more\n", + "than quantifying over elements does elsewhere." + ] + }, { "cell_type": "markdown", "id": "3da49763", diff --git a/notebooks/composition.ipynb b/notebooks/composition.ipynb index 122edbf..6fcf36e 100644 --- a/notebooks/composition.ipynb +++ b/notebooks/composition.ipynb @@ -5,14 +5,17 @@ "id": "dc56966b", "metadata": {}, "source": [ - "# Composing presentations\n", + "# Building new structures from old\n", "\n", "Automatic structures over a shared signature are closed under **disjoint union**\n", "and **direct products**; uniformly automatic classes are closed under **union**\n", - "and under taking all **finite direct products** of their members.\n", + "and under taking all **finite direct products** of their members. They are also\n", + "closed under **first-order interpretation** — defining one structure inside\n", + "another by formulas.\n", "\n", - "`autstr.composition` performs these constructions: each takes presentations and\n", - "returns a presentation, so the result is queried exactly like any other." + "`autstr.composition` and `autstr.interpretations` perform these constructions:\n", + "each takes presentations and returns a presentation, so the result is queried\n", + "exactly like any other." ] }, { @@ -181,6 +184,213 @@ "the cyclic groups; it predates the module, which is a good sign the abstraction\n", "is the right one." ] + }, + { + "cell_type": "markdown", + "id": "a0f1d87e", + "metadata": {}, + "source": [ + "---\n", + "\n", + "## First-order interpretations\n", + "\n", + "An interpretation defines a structure *inside* another one. You give\n", + "\n", + "- a **domain formula** $\\delta(\\bar x)$ saying which tuples of the source are\n", + " elements of the new structure — so an element is a $k$-tuple, and $k$ is the\n", + " interpretation's **dimension**;\n", + "- a formula per **relation**, over $k$ coordinates per argument;\n", + "- optionally an **equivalence** $\\varepsilon(\\bar x, \\bar y)$, and then the\n", + " elements are its classes.\n", + "\n", + "`interpret` does not merely record this: it *computes* the presentation, so the\n", + "result carries real automata and answers queries at full speed.\n", + "\n", + "The textbook example is the construction of the integers from the naturals. A\n", + "pair $(a, b)$ stands for $a - b$, two pairs denote the same integer when\n", + "$a + d = c + b$, and the order is $a + d < c + b$. That is a 2-dimensional\n", + "quotient interpretation of $(\\mathbb{N}, +, <)$ — and here it is." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "ff03cfd1", + "metadata": {}, + "outputs": [], + "source": [ + "from autstr.arithmetic import BuechiArithmetic\n", + "from autstr.interpretations import interpret\n", + "\n", + "N = BuechiArithmetic() # (N, +, <, |2); A(x,y,z) is x + y = z\n", + "pair = ['x0', 'x1', 'y0', 'y1']\n", + "\n", + "SAME = 'exists z.(A(x0,y1,z) and A(y0,x1,z))' # a + d = c + b\n", + "LESS = ('exists s.(exists t.(A(x0,y1,s) and A(y0,x1,t) '\n", + " 'and Lt(s,t)))') # a + d < c + b\n", + "\n", + "Z = interpret(\n", + " N,\n", + " domain=('Eq(x0,x0) and Eq(x1,x1)', ['x0', 'x1']), # every pair is an element\n", + " relations={'Lt': (LESS, pair), 'Eq': (SAME, pair)},\n", + " dimension=2,\n", + " quotient=(SAME, pair),\n", + ")\n", + "\n", + "print('relations:', Z.get_relation_symbols())\n", + "print('no least element (unlike N):', Z.check('exists x.(all y.((not Lt(y,x))))'))\n", + "print('discrete, not dense: ',\n", + " not Z.check('all x.(all y.(Lt(x,y) -> exists z.(Lt(x,z) and Lt(z,y))))'))" + ] + }, + { + "cell_type": "markdown", + "id": "a772b548", + "metadata": {}, + "source": [ + "### A codec says what the elements are\n", + "\n", + "The construction is now correct but illegible: an element of `Z` is a *pair of\n", + "naturals*, and queries hand back the words encoding those pairs. A **codec** is\n", + "the missing half — a pair of functions between Python values and the words that\n", + "represent them. Give one in a `Signature`, and the structure speaks integers.\n", + "\n", + "Every structure the library ships declares its own this way, which is why\n", + "`symbolic()` needs no argument on them. For a structure you build yourself,\n", + "this is what you write." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "53a41a45", + "metadata": {}, + "outputs": [], + "source": [ + "from autstr.symbolic import FunctionCodec, Signature\n", + "\n", + "PAD = '*'\n", + "\n", + "def encode(n):\n", + " \"\"\"n as the pair (a, b) with n = a - b, folded into pair letters.\"\"\"\n", + " a, b = (n, 0) if n >= 0 else (0, -n)\n", + " wa, wb = N.encode(a), N.encode(b) # the source structure's own codec\n", + " width = max(len(wa), len(wb))\n", + " return [(wa[i] if i < len(wa) else PAD, wb[i] if i < len(wb) else PAD)\n", + " for i in range(width)]\n", + "\n", + "def decode(word):\n", + " return (N.decode([letter[0] for letter in word])\n", + " - N.decode([letter[1] for letter in word]))\n", + "\n", + "S = Z.symbolic(Signature(codec=FunctionCodec(encode, decode))\n", + " .operator('lt', 'Lt')\n", + " .operator('eq', 'Eq'))\n", + "x, y = S.vars('x y')\n", + "\n", + "print('-2 < 3 :', (-2, 3) in x.lt(y))\n", + "print(' 3 < -2:', (3, -2) in x.lt(y))\n", + "print('solutions of x < 2:', [t for t, _ in zip(iter(x.lt(2)), range(7))])" + ] + }, + { + "cell_type": "markdown", + "id": "87aa2f42", + "metadata": {}, + "source": [ + "The quotient picks one representative per class — over words, the shortlex-least\n", + "member — so each integer is enumerated once. Over *trees* no order is\n", + "well-founded, and the representative is instead the least **description** of the\n", + "class (Kuske & Weidner); `interpret` handles both, since a tree presentation\n", + "goes in and a tree presentation comes out.\n", + "\n", + "This is how `autstr.ordinals` is built: the ordinals below $\\omega^n$ are three\n", + "formulas over Büchi arithmetic — the reverse-lexicographic order on Cantor\n", + "coefficients — with no automaton authored by hand, and a codec that writes an\n", + "ordinal as its coefficient tuple." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "e8051d42", + "metadata": {}, + "outputs": [], + "source": [ + "from autstr.ordinals import Ordinal\n", + "\n", + "w2 = Ordinal(2) # the ordinals below omega^2\n", + "a, b = w2.symbolic().vars('a b')\n", + "\n", + "# an ordinal is its Cantor coefficients, most significant first:\n", + "# (1, 0) is omega, (0, 5) is 5, (1, 1) is omega + 1\n", + "print('5 < omega: ', ((0, 5), (1, 0)) in a.lt(b))\n", + "print('omega < 5: ', ((1, 0), (0, 5)) in a.lt(b))\n", + "print('omega+1 < omega*2:', ((1, 1), (2, 0)) in a.lt(b))\n", + "print('below omega + 2: ', [t for t, _ in zip(iter(a.lt((1, 2))), range(5))])" + ] + }, + { + "cell_type": "markdown", + "id": "3123dc4e", + "metadata": {}, + "source": [ + "---\n", + "\n", + "## Saving what you built\n", + "\n", + "Every construction on this page *computes* automata, and some of them are not\n", + "cheap. A presentation therefore serializes: `automatic_presentation_to_file`\n", + "writes the whole thing — universe, every relation, the alphabet — and\n", + "`automatic_presentation_from_file` reads it back.\n", + "\n", + "The payload stores each automaton's **transition diagrams** rather than a flat\n", + "`symbol → target` table, so a relation over a convolution alphabet too wide to\n", + "enumerate still writes out in the size of its diagrams." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "46b0fc0c", + "metadata": {}, + "outputs": [], + "source": [ + "import tempfile, os\n", + "from autstr.presentations import AutomaticPresentation\n", + "\n", + "path = os.path.join(tempfile.mkdtemp(), 'integers.autstr')\n", + "Z.automatic_presentation_to_file(path)\n", + "print(f'{os.path.getsize(path)} bytes on disk')\n", + "\n", + "reloaded = AutomaticPresentation.automatic_presentation_from_file(path)\n", + "print('relations:', reloaded.get_relation_symbols())\n", + "\n", + "# the reloaded structure answers the same questions\n", + "R = reloaded.symbolic(Signature(codec=FunctionCodec(encode, decode))\n", + " .operator('lt', 'Lt').operator('eq', 'Eq'))\n", + "a, b = R.vars('a b')\n", + "print('-2 < 3 after a round trip:', (-2, 3) in a.lt(b))\n", + "print('still discrete:',\n", + " not reloaded.check('all x.(all y.(Lt(x,y) -> exists z.(Lt(x,z) and Lt(z,y))))'))" + ] + }, + { + "cell_type": "markdown", + "id": "2bda71d3", + "metadata": {}, + "source": [ + "What a file does **not** carry is the signature: a codec is Python code, not\n", + "data, so a reloaded presentation is a bare structure until you hand it one\n", + "again. Structures that ship with the library declare their own, which is why\n", + "`BuechiArithmeticZ().symbolic()` needs no argument while this one does.\n", + "\n", + "Tree presentations serialize the same way and with the same method names. There\n", + "the payload matters more, because tree relations are where the expensive\n", + "constructions live — the reachability relation of a collapsible pushdown graph\n", + "is exponential in the system's control states, and once built it is worth\n", + "keeping." + ] } ], "metadata": { diff --git a/notebooks/graphs.ipynb b/notebooks/graphs.ipynb index 97f7b9a..87c5dc1 100644 --- a/notebooks/graphs.ipynb +++ b/notebooks/graphs.ipynb @@ -115,6 +115,37 @@ " print(f'{name:30s} bipartite = {cls.check(bipartite, TreeDepthGraph.from_networkx(G))}')" ] }, + { + "cell_type": "markdown", + "id": "b4aff901", + "metadata": {}, + "source": [ + "The same query without the parenthesis soup: `symbolic()` hands out variables and\n", + "relation symbols, and `.implies`, `.all` and `.drop` build the quantifiers. A set\n", + "variable is just a variable — `Subset(x, c)` reads it as a set, which is what makes\n", + "this monadic *second*-order rather than first." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "41259a4b", + "metadata": {}, + "outputs": [], + "source": [ + "S = cls.symbolic()\n", + "c, x, y = S.vars('c x y')\n", + "E, Subset = S.rel('E'), S.rel('Subset')\n", + "\n", + "bipartite_sym = (E(x, y).implies((Subset(x, c) & ~Subset(y, c))\n", + " | (~Subset(x, c) & Subset(y, c)))\n", + " ).all([x, y]).drop(c)\n", + "\n", + "for name, G in cases.items():\n", + " print(f'{name:30s} bipartite = '\n", + " f'{S.check_member(bipartite_sym, cls.advice(TreeDepthGraph.from_networkx(G)))}')" + ] + }, { "cell_type": "markdown", "id": "5826682f", diff --git a/notebooks/groups.ipynb b/notebooks/groups.ipynb index 151f760..a271364 100644 --- a/notebooks/groups.ipynb +++ b/notebooks/groups.ipynb @@ -49,14 +49,51 @@ "from autstr.groups import FiniteAbelianGroups\n", "\n", "ab = FiniteAbelianGroups()\n", - "print('A((1,1),(1,2),(0,0)) in Z2+Z3:', ab.check('A(x,y,z)', [2, 3], x=(1, 1), y=(1, 2), z=(0, 0)))\n", + "print('A((1,1),(1,2),(0,0)) in Z2+Z3:', ab.check('A(x,y,z)', [2, 3], x=(1, 1), y=(1, 2), z=(0, 0)))" + ] + }, + { + "cell_type": "markdown", + "id": "fbb35bc7", + "metadata": {}, + "source": [ + "### The same queries without formula strings\n", "\n", - "# One compiled automaton, evaluated over many groups: \"has an element of order 4\".\n", - "phi = 'exists x.((not A(x,x,x)) and (exists z.(A(x,x,z) and A(z,z,z))))'\n", - "dfa, _ = ab.evaluate(phi)\n", - "for orders in ([4], [3], [2, 3], [5, 6]):\n", + "`symbolic()` hands out variables that compose with Python operators. For an abelian\n", + "class that is `+` and `.eq`; the class has no constants of its own, so the identity is\n", + "named by what defines it, $t + t = t$. One formula compiles **once for the class** and\n", + "then decides any member." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "d985b332", + "metadata": {}, + "outputs": [], + "source": [ + "S = ab.symbolic()\n", + "x, y, z = S.vars('x y z')\n", + "\n", + "is_zero = lambda t: (t + t).eq(t) # a class has no constant symbols\n", + "\n", + "# \"has an element of order 4\": y = 2x, z = 2y = 0, with x and y both nonzero\n", + "order_four = ((x + x).eq(y) & (y + y).eq(z) & is_zero(z)\n", + " & ~is_zero(x) & ~is_zero(y))\n", + "\n", + "for orders in ([4], [2, 2], [3], [2, 3], [8]):\n", " print(f'orders={orders}: has an order-4 element =',\n", - " dfa.accepts([(s,) for s in ab.advice(orders)]))" + " S.check_member(order_four, ab.advice(orders)))" + ] + }, + { + "cell_type": "markdown", + "id": "5b736df5", + "metadata": {}, + "source": [ + "The two groups of order 4 come apart here: $\\mathbb{Z}_4$ has such an element and\n", + "$\\mathbb{Z}_2 \\oplus \\mathbb{Z}_2$ does not — decided by running each group's advice\n", + "word through one automaton." ] }, { diff --git a/notebooks/infinite_structures.ipynb b/notebooks/infinite_structures.ipynb new file mode 100644 index 0000000..7ab7e9d --- /dev/null +++ b/notebooks/infinite_structures.ipynb @@ -0,0 +1,307 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "722dd063", + "metadata": {}, + "source": [ + "# Infinite graphs, and how far first-order logic reaches\n", + "\n", + "The structures in the other notebooks are infinite but tame: arithmetic, orders,\n", + "lattices. This one is about infinite **graphs** — the Cayley graph of\n", + "$\\mathbb{Z}^n$, the infinite $k$-regular tree, the configuration graph of a\n", + "Turing machine, and the configuration graph of a level 2 collapsible pushdown\n", + "system.\n", + "\n", + "The last two are the interesting pair. Both present *computation* as a graph:\n", + "vertices are machine configurations, edges are single steps. Both have a\n", + "decidable first-order theory. But **reachability** — is there a run of any\n", + "length from here to there — is undecidable for the Turing machine and decidable\n", + "for the collapsible pushdown system, and that difference is visible in what the\n", + "library can hand you.\n", + "\n", + "> **Variable naming.** The formula parser treats a name as a variable only if it\n", + "> matches `[a-df-z][0-9]*` — a single lowercase letter (never `e`, which is the\n", + "> parser's event marker), optionally followed by digits." + ] + }, + { + "cell_type": "markdown", + "id": "c6515bc9", + "metadata": {}, + "source": [ + "## The integer grid\n", + "\n", + "$\\mathbb{Z}^n$ with its Cayley graph: vertices are integer points, and two are\n", + "adjacent when they differ by one in a single coordinate. It is built as an\n", + "**asynchronous product** of $n$ copies of $(\\mathbb{Z}, +)$ — the product that\n", + "advances exactly one coordinate and holds the rest, which is precisely a grid\n", + "step." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "c26dad9f", + "metadata": {}, + "outputs": [], + "source": [ + "from autstr.infinite_graphs import IntegerGrid\n", + "\n", + "grid = IntegerGrid(2)\n", + "S = grid.symbolic()\n", + "x, y = S.vars('x y')\n", + "\n", + "print('(0,0) — (0,1):', ((0, 0), (0, 1)) in x.adj(y))\n", + "print('(0,0) — (1,1):', ((0, 0), (1, 1)) in x.adj(y), ' (diagonals are not edges)')\n", + "print('symmetric: ', grid.is_symmetric())\n", + "\n", + "neighbours = [b for (a, b), _ in zip(iter(x.eq((0, 0)) & x.adj(y)), range(4))]\n", + "print('neighbours of the origin:', neighbours)" + ] + }, + { + "cell_type": "markdown", + "id": "1b5bde03", + "metadata": {}, + "source": [ + "Vertices are Python tuples because the structure ships a **codec**: the points\n", + "go in and come out as `(a, b)`, while underneath each is a word over a product\n", + "alphabet." + ] + }, + { + "cell_type": "markdown", + "id": "bc7fa921", + "metadata": {}, + "source": [ + "## The regular tree\n", + "\n", + "The infinite $k$-regular tree $T_k$: vertices are finite words over $k$ letters,\n", + "each with $k$ children. It carries the child relation, the successors `S0`…`S{k-1}`\n", + "individually, and the **prefix order** — an ancestor relation, which is what makes\n", + "it more than a graph." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "a3213a81", + "metadata": {}, + "outputs": [], + "source": [ + "from autstr.infinite_graphs import RegularTree\n", + "\n", + "tree = RegularTree(2)\n", + "print('relations:', tree.get_relation_symbols())\n", + "\n", + "T = tree.symbolic()\n", + "u, v = T.vars('u v')\n", + "print('root — its 0-child: ', ((), (0,)) in u.adj(v))\n", + "print('root is an ancestor: ', tree.check('exists u.(all v.(Prefix(u,v)))'))\n", + "print('nobody is their own child:',\n", + " tree.check('all u.(all v.(Child(u,v) -> (not Eq(u,v))))'))" + ] + }, + { + "cell_type": "markdown", + "id": "19a84ad5", + "metadata": {}, + "source": [ + "## Turing machines: where first-order logic stops\n", + "\n", + "A configuration is a state, a tape and a head position; one step is an edge. The\n", + "step relation is automatic — it rewrites a bounded window of the tape — so the\n", + "whole configuration graph is an automatic structure and its first-order theory\n", + "is decidable.\n", + "\n", + "What you may **not** ask is whether one configuration reaches another. That is\n", + "the halting problem, and no amount of cleverness puts it inside first-order logic\n", + "over this graph. So `autstr.turing` gives you `E` and `Halt`, and stops there." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "eacf10c5", + "metadata": {}, + "outputs": [], + "source": [ + "from autstr.turing import TuringMachine, Configuration\n", + "\n", + "# two states, flipping a bit and stepping right, then back\n", + "flipper = TuringMachine({('a', '0'): ('b', '1', 'R'),\n", + " ('a', '1'): ('b', '0', 'R'),\n", + " ('b', '0'): ('a', '0', 'L'),\n", + " ('b', '1'): ('a', '1', 'L')}, blank='0')\n", + "\n", + "machine = flipper.configuration_graph()\n", + "print('relations: ', machine.get_relation_symbols())\n", + "print('deterministic:', machine.is_deterministic())\n", + "\n", + "start = Configuration('a', ('1', '0'), 0)\n", + "after = flipper.step(start)\n", + "print('one step:', start.state, start.tape, start.head, '->',\n", + " after.state, after.tape, after.head)\n", + "\n", + "M = machine.symbolic()\n", + "p, q = M.vars('p q')\n", + "print('and that step is an edge:', (start, after) in p.adj(q))" + ] + }, + { + "cell_type": "markdown", + "id": "74a3bcf4", + "metadata": {}, + "source": [ + "Determinism *is* first-order — \"every configuration has at most one\n", + "successor\" quantifies over one step, not over runs — so it costs nothing beyond\n", + "`E`. Reachability would quantify over runs of unbounded length, and that is\n", + "exactly the line first-order logic does not cross." + ] + }, + { + "cell_type": "markdown", + "id": "c742b33d", + "metadata": {}, + "source": [ + "## Collapsible pushdown graphs: where reachability comes back\n", + "\n", + "A **level 2 collapsible pushdown system** has a stack of stacks. It can clone\n", + "the topmost word, push a letter carrying a *collapse link* back to the stack it\n", + "was created over, pop, and **collapse** — jump straight back to that stack,\n", + "however far away it now is. These systems generate the level 2 graphs of the\n", + "pushdown hierarchy.\n", + "\n", + "Their configuration graphs are **tree**-automatic rather than string-automatic\n", + "(Kartzow), and that is not a technicality: their MSO theory is undecidable, so\n", + "the tree encoding is the only automatic route to them. A stack of stacks is a\n", + "tree of blocks, and each stack operation is a bounded rewrite at the end of the\n", + "tree's last path.\n", + "\n", + "The payoff is the contrast with the Turing machine above. Here **reachability is\n", + "first-order definable** — a relation of the graph like any other — so you may\n", + "ask about runs of unbounded length." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "3e6a9790", + "metadata": {}, + "outputs": [], + "source": [ + "from autstr.collapsible import Level2CPS\n", + "\n", + "# clone the topmost word, then pop it back off\n", + "system = Level2CPS([('0', None, 'c', '1', 'clone'),\n", + " ('1', None, 'o', '0', 'pop 2')], symbols=('a',))\n", + "graph = system.configuration_graph()\n", + "\n", + "print('relations:', graph.get_relation_symbols())" + ] + }, + { + "cell_type": "markdown", + "id": "82d062e7", + "metadata": {}, + "source": [ + "`Reach` is in that list but not yet built: it is **exponential in the number of\n", + "control states**, so it is declared up front and compiled the first time a query\n", + "mentions it. That deferral is the opt-out — nothing pays for it until it is\n", + "asked for.\n", + "\n", + "Kartzow's construction is a decomposition rather than a fixpoint. Every run\n", + "splits into four stretches — whole words come off the stack, then letters come\n", + "off, then letters go back on, then words go back on — and each stretch is its\n", + "own automaton. All four relations are *reflexive*, so composing them excludes\n", + "nothing, and reachability is the first-order formula\n", + "\n", + "$$\\mathrm{Reach}(x,y) \\;=\\; \\exists d\\, \\exists f\\, \\exists g.\\;\n", + "A(x,d) \\wedge B(d,f) \\wedge C(f,g) \\wedge D(g,y)$$\n", + "\n", + "over the four — no fifth automaton, and no fixpoint over trees." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "d1dc4b5b", + "metadata": {}, + "outputs": [], + "source": [ + "import time\n", + "\n", + "t = time.perf_counter()\n", + "reach = graph.presentation.relation('Reach') # built on first use\n", + "print(f'Reach: {reach.num_states} states, built in {time.perf_counter() - t:.1f}s')\n", + "\n", + "# properties of runs of ANY length -- the questions the Turing graph cannot answer\n", + "print('reflexive: ', graph.check('all x.(Reach(x,x))'))\n", + "print('contains one step:', graph.check('all x.(all y.(E(x,y) -> Reach(x,y)))'))\n", + "print('transitive: ', graph.check(\n", + " 'all x.(all y.(all z.((Reach(x,y) & Reach(y,z)) -> Reach(x,z))))'))" + ] + }, + { + "cell_type": "markdown", + "id": "daec2974", + "metadata": {}, + "source": [ + "Transitivity is worth pausing on. It is a statement about *all* configurations\n", + "and *all* runs between them, decided by automata operations in well under a\n", + "second — and it is not a test that was passed, it is a theorem that was proved.\n", + "\n", + "Constraining the labels a run may read is `reach_along`, which builds Kartzow's\n", + "$\\mathrm{Reach}_L$ by putting the label automaton into a **product system**\n", + "whose ordinary reachability is the answer. An $\\varepsilon$-contraction — any\n", + "number of silent steps followed by one visible one — is the special case of that\n", + "with a two-state label automaton." + ] + }, + { + "cell_type": "markdown", + "id": "5ab0a6b5", + "metadata": {}, + "source": [ + "### Keeping what was expensive\n", + "\n", + "`Reach` cost real work to build, and nothing about it depends on the session.\n", + "Tree presentations serialize exactly as string ones do, so it can be written\n", + "out and read back — the reloaded relation is still reachability." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "1b4ac295", + "metadata": {}, + "outputs": [], + "source": [ + "import tempfile, os\n", + "from autstr.tree_presentations import TreeAutomaticPresentation\n", + "\n", + "path = os.path.join(tempfile.mkdtemp(), 'collapsible.autstr')\n", + "graph.presentation.automatic_presentation_to_file(path)\n", + "print(f'{os.path.getsize(path)} bytes on disk')\n", + "\n", + "reloaded = TreeAutomaticPresentation.automatic_presentation_from_file(path)\n", + "print('Reach is there:', 'Reach' in reloaded.get_relation_symbols())\n", + "print('and still transitive:', reloaded.check(\n", + " 'all x.(all y.(all z.((Reach(x,y) & Reach(y,z)) -> Reach(x,z))))'))" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "name": "python" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/pyproject.toml b/pyproject.toml index 17b795c..9be0573 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "setuptools.build_meta" [project] name = "autstr" -version = "3.1.0" +version = "4.0.0" description = "Library for working with finitely presentable infinite structures" readme = "README.md" authors = [ @@ -73,8 +73,6 @@ testpaths = ["tests"] [tool.setuptools.packages.find] include = ["autstr*"] -[tool.setuptools.package-data] -"autstr.buildin" = ["bin/*.autstr"] [tool.poetry-dynamic-versioning] enable = true diff --git a/scripts/gen_builtin_presentations.py b/scripts/gen_builtin_presentations.py deleted file mode 100644 index 22ac213..0000000 --- a/scripts/gen_builtin_presentations.py +++ /dev/null @@ -1,43 +0,0 @@ -"""Regenerate the serialized built-in presentations in `autstr/buildin/bin`. - -The loaders (`BuechiArithmetic`, `BuechiArithmeticZ`, `MSO0`) deserialize these -artifacts with ``enforce_consistency=False`` — the stored automata are taken to -be already restricted to the universe. So whenever the construction of a -built-in presentation changes, or the consistency preparation itself does, the -artifacts have to be rebuilt from their generators: - - python scripts/gen_builtin_presentations.py [name ...] - -Rewriting an artifact also re-encodes it in the current serializer format, -which is bulkier than the one some of them were written with — so rebuild only -the ones whose content actually changed. -""" -import sys -from pathlib import Path - -from autstr.buildin.presentations import ( - buechi_arithmetic, buechi_arithmetic_Z, finite_powerset, -) - -BIN = Path(__file__).resolve().parent.parent / 'autstr' / 'buildin' / 'bin' - -TARGETS = { - 'buechi.autstr': buechi_arithmetic, - 'buechiZ.autstr': buechi_arithmetic_Z, - 'mso0.autstr': finite_powerset, -} - - -def main(names=()) -> None: - for filename, build in TARGETS.items(): - if names and filename not in names and Path(filename).stem not in names: - continue - presentation = build() - path = BIN / filename - presentation.automatic_presentation_to_file(str(path)) - print(f'{filename}: {len(presentation.automata)} automata ' - f'({", ".join(sorted(presentation.automata))})') - - -if __name__ == '__main__': - main(sys.argv[1:]) diff --git a/scripts/gen_readme_media.py b/scripts/gen_readme_media.py index 1cb6b52..337bd18 100755 --- a/scripts/gen_readme_media.py +++ b/scripts/gen_readme_media.py @@ -12,14 +12,14 @@ """ from pathlib import Path -from autstr.arithmetic import integers +from autstr.arithmetic import BuechiArithmeticZ MEDIA = Path(__file__).resolve().parent.parent / "docs" / "media" def coprime_automaton(primes): """The DFA for {x > 1 : no p in `primes` divides x}.""" - Z = integers() + Z = BuechiArithmeticZ().symbolic() x = Z.var("x") s = x.gt(1) for p in primes: diff --git a/tests/test_arithmetic.py b/tests/test_arithmetic.py index ce308b7..3dbc98d 100644 --- a/tests/test_arithmetic.py +++ b/tests/test_arithmetic.py @@ -3,12 +3,25 @@ import pytest -from autstr.arithmetic import decode, encode, integers +from autstr.arithmetic import BuechiArithmetic, BuechiArithmeticZ +from autstr.powerset import MSO0 + +encode, decode = BuechiArithmeticZ.encode, BuechiArithmeticZ.decode @pytest.fixture(scope='module') def Z(): - return integers() + return BuechiArithmeticZ().symbolic() + + +@pytest.fixture(scope='module') +def N(): + return BuechiArithmetic().symbolic() + + +@pytest.fixture(scope='module') +def sets(): + return MSO0().symbolic() def bounded(formula, limit=6): @@ -159,3 +172,69 @@ def test_enumeration_yields_integers(Z): x, y = Z.vars('x y') formula = (x + y).eq(4) & x.gt(0) & x.lt(y) assert sorted(islice(iter(formula), 5)) == [(1, 3)] + + +# ---------------------------------------------------------------------- +# the naturals: the same interface, without negation +# ---------------------------------------------------------------------- + +@pytest.mark.parametrize('n', [0, 1, 2, 7, 8, 255]) +def test_natural_encode_decode_roundtrip(n): + assert BuechiArithmetic.decode(BuechiArithmetic.encode(n)) == n + + +def test_naturals_reject_negatives(): + with pytest.raises(ValueError): + BuechiArithmetic.encode(-1) + + +def test_naturals_add(N): + x, y = N.vars('x y') + relation = (x + y).eq(12).evaluate() + assert relation.contains(x=5, y=7) + assert not relation.contains(x=5, y=8) + + +def test_naturals_have_a_least_element(N): + x, y = N.vars('x y') + # unbounded above, but 0 has nothing below it -- the difference from Z + assert x.lt(y).drop(y).all(x).check() + assert not y.lt(x).drop(y).all(x).check() + + +# ---------------------------------------------------------------------- +# MSO0: finite sets as Python sets +# ---------------------------------------------------------------------- + +@pytest.mark.parametrize('s', [set(), {0}, {1}, {0, 2}, {0, 1, 2}, {5}]) +def test_set_encode_decode_roundtrip(s): + assert MSO0.decode(MSO0.encode(s)) == s + + +def test_set_encoding_is_canonical(): + # the universe rejects trailing zeros, so {0} is `1`, not `100` + assert MSO0.encode({0}) == ['1'] + assert MSO0.encode({0, 2}) == ['1', '0', '1'] + assert MSO0.encode(set()) == [] + + +def test_set_operations(sets): + x, y, z = sets.vars('x y z') + assert ({0, 1}, {1, 2}, {0, 1, 2}) in (x + y).eq(z) # union + assert ({0, 1}, {1, 2}, {1}) in (x * y).eq(z) # intersection + assert ({0, 1}, {1, 2}, {0}) in (x - y).eq(z) # difference + + +def test_subset_and_singletons(sets): + x, y = sets.vars('x y') + assert ({0, 2}, {0, 1, 2}) in x.subset(y) + assert ({0, 2}, {0, 1}) not in x.subset(y) + assert ({1},) in x.sing() + assert ({0, 1},) not in x.sing() + assert ({1}, {0, 1, 2}) in x.member_of(y) + + +def test_enumeration_yields_sets(sets): + x, y = sets.vars('x y') + solutions = list(islice(iter((x + y).eq({0, 1}) & x.subset(y)), 3)) + assert all(isinstance(a, set) and a | b == {0, 1} for a, b in solutions) diff --git a/tests/test_infinite_graphs.py b/tests/test_infinite_graphs.py index 1233921..d370990 100644 --- a/tests/test_infinite_graphs.py +++ b/tests/test_infinite_graphs.py @@ -8,8 +8,10 @@ """ import pytest -from autstr.arithmetic import decode, encode -from autstr.buildin.presentations import BuechiArithmeticZ +from autstr.arithmetic import BuechiArithmeticZ + +encode, decode = BuechiArithmeticZ.encode, BuechiArithmeticZ.decode +from autstr.arithmetic import BuechiArithmeticZ from autstr.infinite_graphs import InfiniteGraph from autstr.symbolic import FunctionCodec diff --git a/tests/test_interpretations.py b/tests/test_interpretations.py index 0cbdef2..4fd7b50 100644 --- a/tests/test_interpretations.py +++ b/tests/test_interpretations.py @@ -3,8 +3,10 @@ import pytest -from autstr.arithmetic import decode, encode -from autstr.buildin.presentations import BuechiArithmeticZ +from autstr.arithmetic import BuechiArithmeticZ + +encode, decode = BuechiArithmeticZ.encode, BuechiArithmeticZ.decode +from autstr.arithmetic import BuechiArithmeticZ from autstr.infinite_graphs import IntegerGrid, InfiniteGraph from autstr.interpretations import interpret from autstr.symbolic import FunctionCodec diff --git a/tests/test_ordinals.py b/tests/test_ordinals.py index af2a9f2..24400ce 100644 --- a/tests/test_ordinals.py +++ b/tests/test_ordinals.py @@ -132,7 +132,7 @@ def test_repr(self, omega_squared): def test_omega_is_the_naturals(self, omega): # dimension 1: the interpretation is a definable reduct of ℕ, so the # order relation is the source's own, minimized - from autstr.buildin.presentations import BuechiArithmetic + from autstr.arithmetic import BuechiArithmetic assert omega.presentation.automata['Lt'].num_states == \ BuechiArithmetic().automata['Lt'].num_states diff --git a/tests/test_presentations.py b/tests/test_presentations.py index 5298437..18c28a1 100644 --- a/tests/test_presentations.py +++ b/tests/test_presentations.py @@ -10,10 +10,9 @@ import pytest -from autstr.buildin.automata import zero -from autstr.buildin.presentations import ( - BuechiArithmetic, BuechiArithmeticZ, MSO0, -) +from autstr.utils.automata_tools import zero +from autstr.arithmetic import BuechiArithmetic, BuechiArithmeticZ +from autstr.powerset import MSO0 from autstr.interpretations import interpret from autstr.presentations import AutomaticPresentation diff --git a/tests/test_serialization.py b/tests/test_serialization.py index bc863cf..584eb0b 100644 --- a/tests/test_serialization.py +++ b/tests/test_serialization.py @@ -1,6 +1,11 @@ +import json +import struct +import zlib + import numpy as np +import pytest -from autstr.buildin.presentations import BuechiArithmeticZ +from autstr.arithmetic import BuechiArithmeticZ from autstr.sparse_automata import SparseDFA, SparseDFASerializer @@ -52,6 +57,161 @@ def test_round_trip_of_a_multi_tape_automaton(self): assert np.array_equal(reloaded.dense_next(), dfa.dense_next()) def test_the_legacy_flat_payload_still_loads(self): - """BuechiArithmeticZ ships a version-2 file (flat exception rows).""" - presentation = BuechiArithmeticZ() - assert presentation.check('exists x.(A(x,x,x))') # 0 + 0 = 0 + """Version 2 stored a default target plus flat exception rows, before + transitions became shared diagrams. Files written by those versions + must still load, so the payload is built here by hand -- the library + no longer ships one to read. + """ + # a two-state automaton over {0, 1, *}: accepts words ending in 1 + alphabet = sorted({'*', '0', '1'}) + code = {letter: i for i, letter in enumerate(alphabet)} + num_states, max_exceptions = 2, 1 + defaults = np.array([0, 0], dtype=np.uint32) # on anything else + ex_symbols = np.array([[code['1']], [code['1']]], dtype=np.int32) + ex_states = np.array([[1], [1]], dtype=np.int32) + is_accepting = np.array([0, 1], dtype=np.uint8) + + alphabet_json = json.dumps(alphabet).encode('utf-8') + payload = b''.join([ + struct.pack("IIIII", num_states, max_exceptions, 0, 1, + len(alphabet_json)), + alphabet_json, + defaults.tobytes(), + ex_symbols.tobytes(), + ex_states.tobytes(), + is_accepting.tobytes(), + ]) + data = struct.pack("4sB3sII", b'SDFA', 2, b'\0\0\0', + zlib.crc32(payload), len(payload)) + payload + + dfa = SparseDFASerializer.from_bytes(data) + + assert dfa.num_states == 2 + assert dfa.base_alphabet == {'*', '0', '1'} + assert dfa.accepts([('1',)]) + assert dfa.accepts([('0',), ('1',)]) + assert not dfa.accepts([('1',), ('0',)]) + + +class TestProductAlphabet: + """A presentation whose letters are tuples. + + An interpretation of dimension k > 1 encodes an element as a word over the + k-fold product alphabet, so both the alphabet's letters and the padding + symbol are tuples. JSON has no tuples: without restoring them on load, the + alphabet is a set of lists (unhashable) and the padding symbol is a list. + """ + + def _integers_from_naturals(self): + from autstr.arithmetic import BuechiArithmetic + from autstr.interpretations import interpret + pair = ['x0', 'x1', 'y0', 'y1'] + same = 'exists z.(A(x0,y1,z) and A(y0,x1,z))' + less = 'exists s.(exists t.(A(x0,y1,s) and A(y0,x1,t) and Lt(s,t)))' + return interpret( + BuechiArithmetic(), + domain=('Eq(x0,x0) and Eq(x1,x1)', ['x0', 'x1']), + relations={'Lt': (less, pair), 'Eq': (same, pair)}, + dimension=2, quotient=(same, pair)) + + def test_round_trip_through_a_file(self, tmp_path): + from autstr.presentations import AutomaticPresentation + presentation = self._integers_from_naturals() + path = str(tmp_path / 'integers.autstr') + presentation.automatic_presentation_to_file(path) + + reloaded = AutomaticPresentation.automatic_presentation_from_file(path) + + assert set(reloaded.get_relation_symbols()) == \ + set(presentation.get_relation_symbols()) + assert isinstance(reloaded.padding_symbol, tuple) + assert all(isinstance(letter, tuple) for letter in reloaded.sigma) + # the order it presents is still the order of the integers: + # no least element, and discrete rather than dense + assert not reloaded.check( + 'exists x.(all y.((not Lt(y,x)) and (not Eq(x,y))))') + assert not reloaded.check( + 'all x.(all y.(Lt(x,y) -> exists z.(Lt(x,z) and Lt(z,y))))') + assert _same_language(reloaded.automata['Lt'], + presentation.automata['Lt'], max_length=3) + + +class TestTreeSerialization: + """The tree engine's counterpart. + + The compiled form of a tree automaton is a sorted table of child pairs with + one decision-diagram root each, so storing it is storing the pair keys plus + the shared sub-DAG below those roots -- the same payload idea as the string + side, and the same reason for it: a relation over a convolution alphabet + too wide to enumerate still writes out in the size of its diagrams. + """ + + def test_automaton_round_trip(self): + from autstr.sparse_tree_automata import SparseTreeAutomatonSerializer + from autstr.tree_arithmetic import skolem_arithmetic + + original = skolem_arithmetic().automata['M'] # x * y = z + reloaded = SparseTreeAutomatonSerializer.from_bytes( + SparseTreeAutomatonSerializer.to_bytes(original)) + + assert reloaded.num_states == original.num_states + assert reloaded.default_state == original.default_state + assert reloaded.symbol_arity == original.symbol_arity + assert reloaded.base_alphabet_frozen == original.base_alphabet_frozen + assert list(reloaded.is_accepting) == list(original.is_accepting) + assert list(reloaded.pair_keys) == list(original.pair_keys) + + def test_corruption_is_detected(self): + from autstr.sparse_tree_automata import SparseTreeAutomatonSerializer + from autstr.tree_arithmetic import skolem_arithmetic + + data = bytearray(SparseTreeAutomatonSerializer.to_bytes( + skolem_arithmetic().automata['U'])) + data[-1] ^= 0xFF # flip a byte of the payload + with pytest.raises(ValueError, match='corruption'): + SparseTreeAutomatonSerializer.from_bytes(bytes(data)) + + def test_presentation_round_trip_answers_the_same_questions(self, tmp_path): + from autstr.tree_arithmetic import skolem_arithmetic + from autstr.tree_presentations import TreeAutomaticPresentation + + skolem = skolem_arithmetic() + path = str(tmp_path / 'skolem.autstr') + skolem.automatic_presentation_to_file(path) + + reloaded = TreeAutomaticPresentation.automatic_presentation_from_file(path) + + assert set(reloaded.get_relation_symbols()) == \ + set(skolem.get_relation_symbols()) + assert reloaded.padding_symbol == skolem.padding_symbol + for phi in ('exists x.(all y.(M(x,y,y)))', # a multiplicative unit + 'all x.(exists y.(M(x,y,x)))'): + assert reloaded.check(phi) == skolem.check(phi) + + # the signature is not stored, so hand the reloaded structure the + # original's and check that elements still mean what they meant + S = reloaded.symbolic(skolem.default_signature()) + x, y, z = S.vars('x y z') + assert (6, 35, 210) in (x * y).eq(z) + assert (6, 35, 211) not in (x * y).eq(z) + + def test_an_expensive_relation_survives(self, tmp_path): + """The case this exists for: `Reach` costs real time to build, and a + reloaded copy must still be the reachability relation.""" + from autstr.collapsible import Level2CPS + from autstr.tree_presentations import TreeAutomaticPresentation + + system = Level2CPS([('0', None, 'c', '1', 'clone'), + ('1', None, 'o', '0', 'pop 2')], symbols=('a',)) + presentation = system.configuration_graph().presentation + presentation.relation('Reach') # build it + + path = str(tmp_path / 'reach.autstr') + presentation.automatic_presentation_to_file(path) + reloaded = TreeAutomaticPresentation.automatic_presentation_from_file(path) + + assert 'Reach' in reloaded.get_relation_symbols() + assert reloaded.check('all x.(Reach(x,x))') + assert reloaded.check('all x.(all y.(E(x,y) -> Reach(x,y)))') + assert reloaded.check( + 'all x.(all y.(all z.((Reach(x,y) & Reach(y,z)) -> Reach(x,z))))') diff --git a/tests/test_skolem.py b/tests/test_skolem.py index e49e080..3c9a8e5 100644 --- a/tests/test_skolem.py +++ b/tests/test_skolem.py @@ -3,7 +3,7 @@ import pytest -from autstr.buildin.tree_presentations import SkolemArithmetic, _prime +from autstr.tree_arithmetic import SkolemArithmetic, _prime from autstr.sparse_tree_automata import Tree enc = SkolemArithmetic.encode diff --git a/tests/test_symbolic.py b/tests/test_symbolic.py index 4f0abe1..54ff991 100644 --- a/tests/test_symbolic.py +++ b/tests/test_symbolic.py @@ -3,7 +3,7 @@ import pytest -from autstr.buildin.presentations import BuechiArithmeticZ +from autstr.arithmetic import BuechiArithmeticZ from autstr.symbolic import ( CompileError, FunctionCodec, Signature, SymbolicSymbolError, graph_signature, order_signature, relational_signature, @@ -330,11 +330,19 @@ def test_bare_structure_needs_no_signature(): def test_constants_need_a_codec(): - S = BuechiArithmeticZ().symbolic() + # a signature that declares no codec cannot turn a Python value into an + # element, even over a structure whose own signature would + S = BuechiArithmeticZ().symbolic(Signature()) with pytest.raises(SymbolicSymbolError, match='no element codec'): S.const(3) +def test_the_structures_own_signature_brings_a_codec(): + S = BuechiArithmeticZ().symbolic() + x, = S.vars('x') + assert (3,) in x.eq(3) + + # ---------------------------------------------------------------------- # uniformly automatic classes # ---------------------------------------------------------------------- diff --git a/tests/test_symbolic_tree.py b/tests/test_symbolic_tree.py index 5c7fbf8..82f0300 100644 --- a/tests/test_symbolic_tree.py +++ b/tests/test_symbolic_tree.py @@ -8,7 +8,7 @@ import pytest -from autstr.buildin.tree_presentations import SkolemArithmetic +from autstr.tree_arithmetic import SkolemArithmetic from autstr.sparse_tree_automata import convolve_trees from autstr.symbolic import ( CompileError, FunctionCodec, Signature, SymbolicSymbolError, diff --git a/tests/test_tree_interpretations.py b/tests/test_tree_interpretations.py index 789a9b6..f47d4fa 100644 --- a/tests/test_tree_interpretations.py +++ b/tests/test_tree_interpretations.py @@ -16,7 +16,7 @@ import pytest -from autstr.buildin.tree_presentations import SkolemArithmetic +from autstr.tree_arithmetic import SkolemArithmetic from autstr.interpretations import _EQUIV, _tree_representatives, interpret from autstr.sparse_tree_automata import Tree, convolve_trees from autstr.tree_presentations import TreeAutomaticPresentation diff --git a/tests/test_tree_presentations.py b/tests/test_tree_presentations.py index d2019e6..e3965b3 100644 --- a/tests/test_tree_presentations.py +++ b/tests/test_tree_presentations.py @@ -3,7 +3,7 @@ import numpy as np import pytest -from autstr.buildin.presentations import BuechiArithmeticZ +from autstr.arithmetic import BuechiArithmeticZ from autstr.sparse_automata import SparseDFA from autstr.sparse_tree_automata import Tree from autstr.tree_presentations import TreeAutomaticPresentation