Created
February 16, 2026 18:38
-
-
Save laserbat/fd08f3d2c867cdd8b157fb7214d21cdc to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/python3 | |
| from __future__ import annotations | |
| import copy | |
| import string | |
| from collections.abc import Callable | |
| from enum import Enum, auto | |
| from functools import cached_property | |
| from types import MappingProxyType | |
| class ExprKind(Enum): | |
| ATOM = auto() | |
| UNARY = auto() | |
| BINARY = auto() | |
| VARIABLE = auto() | |
| CONSTANT = auto() | |
| UNKNOWN = auto() | |
| class Expr: | |
| a: Expr | |
| b: Expr | |
| name: str | |
| kind: ExprKind | |
| _beta_rules: MappingProxyType[str, Callable[[*tuple[Expr, ...]], Expr]] | |
| __slots__ = ["a", "b", "name", "kind", "_beta_rules", "__dict__"] | |
| def __init__(self) -> None: | |
| self.kind = ExprKind.UNKNOWN | |
| self.name = "unknown" | |
| self._beta_rules = MappingProxyType({}) | |
| def __xor__(self, other: Expr) -> Xor: | |
| return Xor(self, other) | |
| def __and__(self, other: Expr) -> And: | |
| return And(self, other) | |
| def __neg__(self) -> Neg: | |
| return Neg(self) | |
| def __matmul__(self, other: Expr) -> MatMul: | |
| return MatMul(self, other) | |
| def __rshift__(self, other: Expr) -> Fwd: | |
| return Fwd(self, other) | |
| def __lshift__(self, other: Expr) -> Bwd: | |
| return Bwd(self, other) | |
| def _pretty(self, root: bool = False) -> str: | |
| match self.kind: | |
| case ExprKind.BINARY: | |
| pretty_a = self.a._pretty() | |
| pretty_b = self.b._pretty() | |
| out = f"{pretty_a} {self.name} {pretty_b}" | |
| if not root: | |
| out = f"({out})" | |
| case ExprKind.UNARY: | |
| pretty_a = self.a._pretty() | |
| out = f"{self.name}{pretty_a}" | |
| case ExprKind.ATOM: | |
| out = f"Atom({self.name})" | |
| case ExprKind.CONSTANT: | |
| out = f"{self.name}" | |
| case ExprKind.VARIABLE: | |
| out = f"{self.name}" | |
| case ExprKind.UNKNOWN: | |
| raise ValueError("cannot pretty-print an undefined expression") | |
| if self.is_redex(): | |
| return f"[{out}]" | |
| return out | |
| def __repr__(self) -> str: | |
| return self._pretty(True) | |
| @cached_property | |
| def _spine(self) -> tuple[Expr, str, tuple[Expr, ...]]: | |
| if self.kind != ExprKind.BINARY: | |
| return (self, "", ()) | |
| is_fwd = isinstance(self, Fwd) | |
| is_bwd = isinstance(self, Bwd) | |
| if not is_fwd and not is_bwd: | |
| return (self, "", ()) | |
| head, path, values = self.a._spine | |
| direction = ">" | |
| if is_bwd: | |
| direction = "<" | |
| return (head, path + direction, values + (self.b,)) | |
| def is_redex(self) -> bool: | |
| head, path, _ = self._spine | |
| for rule_path in head._beta_rules: | |
| if rule_path == path: | |
| return True | |
| return False | |
| def with_(self, **kw: Expr) -> Expr: | |
| new = copy.copy(self) | |
| for k, v in kw.items(): | |
| setattr(new, k, v) | |
| new.__dict__.pop("_spine", None) | |
| return new | |
| def reduce_once(self) -> tuple[Expr, bool]: | |
| node = self | |
| def do_reduce(n: Expr) -> Expr: | |
| head, path, values = n._spine | |
| match head.kind: | |
| case ExprKind.BINARY: | |
| return head._beta_rules[path](head.a, head.b, *values) | |
| case ExprKind.UNARY: | |
| return head._beta_rules[path](head.a, *values) | |
| case _: | |
| return head._beta_rules[path](*values) | |
| if node.is_redex(): | |
| return do_reduce(node), True | |
| match node.kind: | |
| case ExprKind.BINARY: | |
| new_a, changed = node.a.reduce_once() | |
| if changed: | |
| return node.with_(a=new_a), True | |
| new_b, changed = node.b.reduce_once() | |
| if changed: | |
| return node.with_(b=new_b), True | |
| return node, False | |
| case ExprKind.UNARY: | |
| new_a, changed = node.a.reduce_once() | |
| if changed: | |
| return node.with_(a=new_a), True | |
| return node, False | |
| case _: | |
| return node, False | |
| class Atom(Expr): | |
| def __init__(self, name: str) -> None: | |
| super().__init__() | |
| self.name = name | |
| self.kind = ExprKind.ATOM | |
| class Var(Expr): | |
| def __init__(self, name: str) -> None: | |
| super().__init__() | |
| if not name or name[0] not in string.ascii_uppercase: | |
| raise ValueError("variable names must start with an uppercase letter") | |
| self.name = name | |
| self.kind = ExprKind.VARIABLE | |
| class Xor(Expr): | |
| def __init__(self, a: Expr, b: Expr) -> None: | |
| super().__init__() | |
| self.a = a | |
| self.b = b | |
| self.name = "^" | |
| self.kind = ExprKind.BINARY | |
| # r1: (A + B) > C = (B > ((A < ((B * #C) > r)) < C)) > C | |
| # r2: (A + B) < C = (B > ((A > ((((r * s) > B) * #C) > r)) < C)) < C | |
| def _rule1(a: Expr, b: Expr, c: Expr, *_: Expr): | |
| return (b >> ((a << ((b @ -c) >> refl)) << c)) >> c | |
| def _rule2(a: Expr, b: Expr, c: Expr, *_: Expr): | |
| return (b >> ((a >> ((((refl @ sym) >> b) @ -c) >> refl)) << c)) << c | |
| self._beta_rules = MappingProxyType({">": _rule1, "<": _rule2}) | |
| class And(Expr): | |
| def __init__(self, a: Expr, b: Expr) -> None: | |
| super().__init__() | |
| self.a = a | |
| self.b = b | |
| self.name = "&" | |
| self.kind = ExprKind.BINARY | |
| # r1: (A - B) > C = (B > C) > C | |
| # r2: (A - B) < C = (B > #(C < A)) < C | |
| def _rule1(_a: Expr, b: Expr, c: Expr, *_: Expr): | |
| return (b >> c) >> c | |
| def _rule2(a: Expr, b: Expr, c: Expr, *_: Expr): | |
| return (b >> -(c << a)) << c | |
| self._beta_rules = MappingProxyType({">": _rule1, "<": _rule2}) | |
| class MatMul(Expr): | |
| def __init__(self, a: Expr, b: Expr) -> None: | |
| super().__init__() | |
| self.a = a | |
| self.b = b | |
| self.name = "@" | |
| self.kind = ExprKind.BINARY | |
| # r1: ((A * B) > C) > D = B > (C > (A > D)) | |
| # r2: ((A * B) > C) < D = A < (C < (B < D)) | |
| # r3: ((A * B) < C) > D = B < (C > (A < D)) | |
| # r4: ((A * B) < C) < D = A > (C < (B > D)) | |
| def _rule1(a: Expr, b: Expr, c: Expr, d: Expr, *_: Expr): | |
| return b >> (c >> (a >> d)) | |
| def _rule2(a: Expr, b: Expr, c: Expr, d: Expr, *_: Expr): | |
| return a << (c << (b << d)) | |
| def _rule3(a: Expr, b: Expr, c: Expr, d: Expr, *_: Expr): | |
| return b << (c >> (a << d)) | |
| def _rule4(a: Expr, b: Expr, c: Expr, d: Expr, *_: Expr): | |
| return a >> (c << (b >> d)) | |
| self._beta_rules = MappingProxyType({">>": _rule1, "><": _rule2, "<>": _rule3, "<<": _rule4}) | |
| class Fwd(Expr): | |
| def __init__(self, a: Expr, b: Expr) -> None: | |
| super().__init__() | |
| self.a = a | |
| self.b = b | |
| self.name = ">>" | |
| self.kind = ExprKind.BINARY | |
| class Bwd(Expr): | |
| def __init__(self, a: Expr, b: Expr) -> None: | |
| super().__init__() | |
| self.a = a | |
| self.b = b | |
| self.name = "<<" | |
| self.kind = ExprKind.BINARY | |
| class Neg(Expr): | |
| def __init__(self, a: Expr) -> None: | |
| super().__init__() | |
| self.a = a | |
| self.name = "-" | |
| self.kind = ExprKind.UNARY | |
| # r1: #A > B = B > A | |
| # r2: (#A < B) > C = B | |
| # r3: (#A < B) < C = A | |
| def _rule1(a: Expr, b: Expr, *_: Expr): | |
| return b >> a | |
| def _rule2(_a: Expr, b: Expr, *_: Expr): | |
| return b | |
| def _rule3(a: Expr, *_: Expr): | |
| return a | |
| self._beta_rules = MappingProxyType({">": _rule1, "<>": _rule2, "<<": _rule3}) | |
| class Refl(Expr): | |
| def __init__(self) -> None: | |
| super().__init__() | |
| self.name = "refl" | |
| self.kind = ExprKind.CONSTANT | |
| # r1: r > A = A | |
| # r2: r < A = A | |
| def _rule1(a: Expr, *_: Expr): | |
| return a | |
| self._beta_rules = MappingProxyType({">": _rule1, "<": _rule1}) | |
| class Sym(Expr): | |
| def __init__(self) -> None: | |
| super().__init__() | |
| self.name = "sym" | |
| self.kind = ExprKind.CONSTANT | |
| # r1: (s > A) > B = A < B | |
| # r2: (s > A) < B = A > B | |
| # r3: (s < A) > B = A < B | |
| # r4: (s < A) < B = A > B | |
| def _rule1(a: Expr, b: Expr, *_: Expr): | |
| return a << b | |
| def _rule2(a: Expr, b: Expr, *_: Expr): | |
| return a >> b | |
| self._beta_rules = MappingProxyType({">>": _rule1, "><": _rule2, "<>": _rule1, "<<": _rule2}) | |
| class Dist(Expr): | |
| def __init__(self) -> None: | |
| super().__init__() | |
| self.name = "dist" | |
| self.kind = ExprKind.CONSTANT | |
| # r1: ((d > A) > B) > C = ((A > C) > C) > (B > C) | |
| # r2: ((d > A) > B) < C = A < ((r * s) > (((s > B) * #C) < r)) | |
| # r3: ((d > A) < B) > C = ((A > C) > C) < (B > C) | |
| # r4: ((d > A) < B) < C = A < (((s > B) * #C) < r) | |
| # r5: (d < A) > B = #B < (s > (((s > ((A * #B) > r)) * #B) > r)) | |
| # r6: (d < A) < B = B < (A + B) | |
| def _rule1(a: Expr, b: Expr, c: Expr, *_: Expr): | |
| return ((a >> c) >> c) >> (b >> c) | |
| def _rule2(a: Expr, b: Expr, c: Expr, *_: Expr): | |
| return a << ((refl @ sym) >> (((sym >> b) @ -c) << refl)) | |
| def _rule3(a: Expr, b: Expr, c: Expr, *_: Expr): | |
| return ((a >> c) >> c) << (b >> c) | |
| def _rule4(a: Expr, b: Expr, c: Expr, *_: Expr): | |
| return a << (((sym >> b) @ -c) << refl) | |
| def _rule5(a: Expr, b: Expr, *_: Expr): | |
| return -b << (sym >> (((sym >> ((a @ -b) >> refl)) @ -b) >> refl)) | |
| def _rule6(a: Expr, b: Expr, *_: Expr): | |
| return b << (a ^ b) | |
| self._beta_rules = MappingProxyType( | |
| {">>>": _rule1, ">><": _rule2, "><>": _rule3, "><<": _rule4, "<>": _rule5, "<<": _rule6} | |
| ) | |
| class Flap(Expr): | |
| def __init__(self) -> None: | |
| super().__init__() | |
| self.name = "flap" | |
| self.kind = ExprKind.CONSTANT | |
| # r1: f > A = (r * s) > (s > #A) | |
| # r2: (f < A) > B = ((A > #B) > #B) > B | |
| # r3: (f < A) < B = ((A > (A < (B - A))) > (A < (B - A))) < B | |
| def _rule1(a: Expr, *_: Expr): | |
| return (refl @ sym) >> (sym >> -a) | |
| def _rule2(a: Expr, b: Expr, *_: Expr): | |
| return ((a >> -b) >> -b) >> b | |
| def _rule3(a: Expr, b: Expr, *_: Expr): | |
| return ((a >> (a << (b & a))) >> (a << (b & a))) << b | |
| self._beta_rules = MappingProxyType({">": _rule1, "<>": _rule2, "<<": _rule3}) | |
| refl = Refl() | |
| sym = Sym() | |
| dist = Dist() | |
| flap = Flap() | |
| examples = [ | |
| ( | |
| (((-sym @ (refl >> refl)) @ --sym) @ ---flap) | |
| @ (((flap ^ ---sym) @ (-flap << (refl >> refl))) >> (-refl >> ((refl >> flap) << sym))) | |
| ) | |
| >> (-(((-refl << flap) << dist) >> ((flap >> sym) >> -flap)) ^ flap), | |
| ((dist << (sym << (dist >> dist))) << sym) | |
| << ( | |
| (dist >> (sym << (dist << sym))) | |
| << ((((dist >> dist) << sym) << (flap << sym)) >> ((sym >> flap) << (dist >> (dist >> sym)))) | |
| ), | |
| (flap << (dist << dist)) << (flap << sym), | |
| ((dist) << (sym >> dist)) << ((dist << dist)), | |
| flap | |
| << ( | |
| dist | |
| << (((dist << sym) >> ((dist >> (flap >> (dist << sym))) << sym)) >> ((dist >> (flap >> (dist << sym))) << sym)) | |
| ), | |
| ] | |
| for expression in examples: | |
| print("====") | |
| print(f"example: {expression}") | |
| while True: | |
| print(expression) | |
| expression, reduced = expression.reduce_once() | |
| if not reduced: | |
| break | |
| print("----") | |
| expression = expression >> Var("A") | |
| while True: | |
| print(expression) | |
| expression, reduced = expression.reduce_once() | |
| if not reduced: | |
| break |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment