Innermost reduction in Python
Always contracts an innermost redex, one with no redex in its arguments.
- File
innermost_reduction.py, 143 lines- Level
- I0 not checked yet
- Toolchain
- Python 3.14, pytest 9
- Test framework
- pytest
- Run the tests
python3 -m pytest
# SPDX-License-Identifier: MIT
# Part of https://algorithm.tamnd.com/innermost-reduction/. The authors are listed in prov/KTF62M.jsonl.
"""Leftmost-innermost reduction of first-order terms.
A term is a variable, written as a str, or an application, written as a tuple
(f, t1, ..., tn) whose first item is the function symbol; a constant a is
("a",). A rule is a pair (l, r) of terms where l is not a variable and every
variable of r occurs in l. Positions are tuples of 1-based argument indexes.
All functions use explicit stacks, so deep terms do not hit the recursion limit.
Terms built by a rule share the subterms bound to its variables.
"""
from typing import Optional, Union
Term = Union[str, tuple]
Rule = tuple[Term, Term]
Position = tuple[int, ...]
def is_var(t: Term) -> bool:
return isinstance(t, str)
def variables(t: Term) -> set[str]:
out: set[str] = set()
stack = [t]
while stack:
u = stack.pop()
if is_var(u):
out.add(u)
else:
stack.extend(u[1:])
return out
def term_eq(s: Term, t: Term) -> bool:
"""Syntactic equality, without recursion."""
stack = [(s, t)]
while stack:
u, v = stack.pop()
if u is v:
continue
if is_var(u) or is_var(v):
if u != v:
return False
continue
if len(u) != len(v) or u[0] != v[0]:
return False
stack.extend(zip(u[1:], v[1:]))
return True
def match(pattern: Term, term: Term) -> Optional[dict[str, Term]]:
"""Return sigma with pattern sigma = term, or None. Non-linear patterns
need equal subterms at all occurrences of a variable."""
sigma: dict[str, Term] = {}
stack = [(pattern, term)]
while stack:
p, t = stack.pop()
if is_var(p):
if p in sigma:
if not term_eq(sigma[p], t):
return None
else:
sigma[p] = t
elif is_var(t) or len(p) != len(t) or p[0] != t[0]:
return None
else:
stack.extend(zip(p[1:], t[1:]))
return sigma
def check_rules(rules: list[Rule]) -> None:
for i, (l, r) in enumerate(rules):
if is_var(l):
raise ValueError(f"rule {i}: the left side is a variable")
if not variables(r) <= variables(l):
raise ValueError(f"rule {i}: a variable of the right side is not on the left side")
def _position(link: Optional[tuple]) -> Position:
out: list[int] = []
while link is not None:
link, i = link
out.append(i)
return tuple(reversed(out))
def innermost_normalize(
t: Term,
rules: list[Rule],
max_steps: Optional[int] = None,
trace: Optional[list[tuple[Position, int]]] = None,
) -> tuple[Optional[Term], int]:
"""Reduce t by leftmost-innermost steps, with the first matching rule.
Returns (normal form, number of steps), or (None, max_steps) when the
bound is reached before a normal form. When trace is a list, each step
is appended to it as (position, rule index).
"""
check_rules(rules)
# A position is kept as a linked list (parent, index), with None for the
# root, so that moving one level down costs O(1).
steps = 0 # @line L1
# A task is ("eval", u, sigma, p): normalize u sigma at position p, where the
# values of sigma are normal forms; or ("build", f, n, p).
tasks: list[tuple] = [("eval", t, None, None)]
vals: list[Term] = []
while tasks: # @line L2
task = tasks.pop() # @line L3
if task[0] == "eval":
_, u, sigma, p = task
if is_var(u): # @line L4
vals.append(sigma[u] if sigma is not None and u in sigma else u)
else: # @line L5
n = len(u) - 1
tasks.append(("build", u[0], n, p))
for i in range(n, 0, -1):
tasks.append(("eval", u[i], sigma, (p, i)))
else:
_, f, n, p = task
args = vals[len(vals) - n:] if n else [] # @line L6
del vals[len(vals) - n:]
s = (f, *args)
found = None
for idx, (l, r) in enumerate(rules): # @line L7
tau = match(l, s)
if tau is not None:
found = (idx, r, tau)
break
if found is None: # @line L8
vals.append(s)
elif max_steps is not None and steps >= max_steps: # @line L9
return None, steps
else:
idx, r, tau = found
steps += 1 # @line L10
if trace is not None:
trace.append((_position(p), idx))
tasks.append(("eval", r, tau, p))
return vals.pop(), steps # @line L11
test_innermost_reduction.py 209 lines
# SPDX-License-Identifier: MIT
# Part of https://algorithm.tamnd.com/innermost-reduction/. The authors are listed in prov/KTF62M.jsonl.
import random
import pytest
from innermost_reduction import innermost_normalize, term_eq
# Peano addition and multiplication, the example of the page.
ARITH = [
(("add", ("0",), "y"), "y"),
(("add", ("s", "x"), "y"), ("s", ("add", "x", "y"))),
(("mul", ("0",), "y"), ("0",)),
(("mul", ("s", "x"), "y"), ("add", ("mul", "x", "y"), "y")),
]
def num(k):
t = ("0",)
for _ in range(k):
t = ("s", t)
return t
# ---------- an independent, naive oracle (recursive, for small terms) ----------
def o_match(p, t, s):
if isinstance(p, str):
if p in s:
return s[p] == t
s[p] = t
return True
if isinstance(t, str) or p[0] != t[0] or len(p) != len(t):
return False
return all(o_match(a, b, s) for a, b in zip(p[1:], t[1:]))
def o_subst(t, s):
if isinstance(t, str):
return s.get(t, t)
return (t[0],) + tuple(o_subst(a, s) for a in t[1:])
def o_positions(t, p=()):
yield p, t
if not isinstance(t, str):
for i, a in enumerate(t[1:], 1):
yield from o_positions(a, p + (i,))
def o_replace(t, p, u):
if not p:
return u
i = p[0]
return t[:i] + (o_replace(t[i], p[1:], u),) + t[i + 1:]
def o_rule_at(u, rules):
for k, (l, r) in enumerate(rules):
s = {}
if o_match(l, u, s):
return k, o_subst(r, s)
return None
def o_innermost(t, rules, bound):
"""Leftmost-innermost by brute force: list all redexes, keep those with no
redex strictly below, take the leftmost."""
trace = []
while True:
if sum(1 for _ in o_positions(t)) > 300:
return "big", trace
redexes = [p for p, u in o_positions(t) if o_rule_at(u, rules) is not None]
if not redexes:
return t, trace
inner = [p for p in redexes if not any(q != p and q[:len(p)] == p for q in redexes)]
p = min(inner)
if len(trace) == bound:
return None, trace
u = dict(o_positions(t))[p]
k, v = o_rule_at(u, rules)
trace.append((p, k))
t = o_replace(t, p, v)
def o_successors(t, rules):
out = []
for p, u in o_positions(t):
for l, r in rules:
s = {}
if o_match(l, u, s):
out.append(o_replace(t, p, o_subst(r, s)))
return out
def o_reach(t, rules, limit=300):
seen, todo = {t}, [t]
while todo and len(seen) < limit:
u = todo.pop()
for v in o_successors(u, rules):
if v not in seen:
seen.add(v)
todo.append(v)
return seen
# ---------- tests ----------
def test_page_example():
t = ("mul", num(2), num(1))
trace = []
nf, steps = innermost_normalize(t, ARITH, trace=trace)
assert term_eq(nf, num(2))
assert steps == 6
assert trace == [((), 3), ((1,), 3), ((1, 1), 2), ((1,), 0), ((), 1), ((1,), 0)]
def test_empty_system_and_normal_forms():
t = ("f", "x", ("g", ("a",)))
assert innermost_normalize(t, []) == (t, 0)
assert innermost_normalize("x", ARITH) == ("x", 0)
assert innermost_normalize(num(3), ARITH) == (num(3), 0)
def test_not_normalizing():
rules = [(("f", "x"), ("a",)), (("b",), ("b",))]
nf, steps = innermost_normalize(("f", ("b",)), rules, max_steps=100)
assert nf is None and steps == 100
# the term has the normal form a, reached by one outermost step
assert ("a",) in o_reach(("f", ("b",)), rules)
def test_nonlinear_and_shared_variables():
rules = [(("eq", "x", "x"), ("t",)), (("d", "x"), ("p", "x", "x"))]
nf, _ = innermost_normalize(("eq", ("d", ("a",)), ("p", ("a",), ("a",))), rules)
assert nf == ("t",)
nf, _ = innermost_normalize(("eq", ("a",), ("b",)), rules)
assert nf == ("eq", ("a",), ("b",))
def test_bad_rules():
with pytest.raises(ValueError):
innermost_normalize(("a",), [("x", ("a",))])
with pytest.raises(ValueError):
innermost_normalize(("a",), [(("a",), "y")])
def test_deep_terms():
n = 20000
nf, steps = innermost_normalize(("add", num(n), num(n)), ARITH)
assert steps == n + 1
assert term_eq(nf, num(2 * n))
deep = ("a",)
for _ in range(n):
deep = ("g", deep)
rules = [(("g", ("a",)), ("a",))]
nf, steps = innermost_normalize(deep, rules)
assert nf == ("a",) and steps == n
SIG = [("f", 2), ("g", 1), ("h", 1), ("a", 0), ("b", 0)]
def rand_term(rng, depth, vs):
if depth == 0 or rng.random() < 0.3:
if vs and rng.random() < 0.5:
return rng.choice(vs)
return (rng.choice(["a", "b"]),)
f, n = rng.choice(SIG[:3])
return (f,) + tuple(rand_term(rng, depth - 1, vs) for _ in range(n))
def rand_rules(rng):
rules = []
for _ in range(rng.randint(0, 4)):
while True:
l = rand_term(rng, 2, ["x", "y"])
if not isinstance(l, str):
break
lv = sorted({u for _, u in o_positions(l) if isinstance(u, str)})
r = rand_term(rng, 2, lv)
rules.append((l, r))
return rules
def test_random_against_oracle():
rng = random.Random(20261106)
bound = 30
compared = 0
for _ in range(1500):
rules = rand_rules(rng)
t = rand_term(rng, 3, ["x", "y"])
trace = []
nf, steps = innermost_normalize(t, rules, max_steps=bound, trace=trace)
o_nf, o_trace = o_innermost(t, rules, bound)
if o_nf == "big":
assert trace[:len(o_trace)] == o_trace
continue
compared += 1
assert trace == o_trace
assert nf == o_nf
if nf is not None:
assert steps == len(trace)
assert not o_successors(nf, rules)
reach = o_reach(t, rules, 200)
if len(reach) < 200:
assert nf in reach
assert compared >= 1000
What the next level needs
- the tests did not run in this build