Skip to content

Instantly share code, notes, and snippets.

@LeeeeT

LeeeeT/ic.py

Last active January 5, 2026 04:44
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save LeeeeT/8ded48125c6e8488d1b21dc22e6abeba to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save LeeeeT/8ded48125c6e8488d1b21dc22e6abeba to your computer and use it in GitHub Desktop.
Download ZIP
k-SIC + universal δ + UDP rotations
Raw
ic.py
import itertools
from dataclasses import dataclass
type Name = int
name = itertools.count()
type Label = int
label = itertools.count()
type Term = Pos | Neg
type Pos = Var | Nil | Lam | Sup | Usp | Dp0 | Dp1
type Neg = Sub | Era | App | Dup | Udp
@dataclass(frozen=True)
class Var:
nam: Name
@dataclass(frozen=True)
class Sub:
nam: Name
@dataclass(frozen=True)
class Nil:
pass
@dataclass(frozen=True)
class Era:
pass
@dataclass(frozen=True)
class Lam:
bnd: Neg
bod: Pos
@dataclass(frozen=True)
class App:
arg: Pos
ret: Neg
@dataclass(frozen=True)
class Dup:
dpl: Label
dp0: Neg
dp1: Neg
@dataclass(frozen=True)
class Sup:
spl: Label
sp0: Pos
sp1: Pos
@dataclass(frozen=True)
class Udp:
ud0: Neg
ud1: Neg
@dataclass(frozen=True)
class Usp:
us0: Pos
us1: Pos
@dataclass(frozen=True)
class Dp0:
bnd: Neg
bod: Pos
@dataclass(frozen=True)
class Dp1:
bod: Pos
bnd: Neg
def show(term: Term, vars: dict[Name, Pos] = {}, subs: dict[Name, Neg] = {}) -> str:
match term:
case Var(nam) if nam in vars:
return show(vars[nam], vars, subs)
case Var(nam):
return f"+{nam}"
case Sub(nam) if nam in subs:
return show(subs[nam], vars, subs)
case Sub(nam):
return f"-{nam}"
case Nil():
return "+_"
case Era():
return "-_"
case Lam(bnd, bod):
return f"+({show(bnd, vars, subs)} {show(bod, vars, subs)})"
case App(arg, ret):
return f"-({show(arg, vars, subs)} {show(ret, vars, subs)})"
case Dup(dpl, dp0, dp1):
return f"-&{dpl}{{{show(dp0, vars, subs)} {show(dp1, vars, subs)}}}"
case Sup(spl, sp0, sp1):
return f"+&{spl}{{{show(sp0, vars, subs)} {show(sp1, vars, subs)}}}"
case Udp(ud0, ud1):
return f"-{{{show(ud0, vars, subs)} {show(ud1, vars, subs)}}}"
case Usp(us0, us1):
return f"+{{{show(us0, vars, subs)} {show(us1, vars, subs)}}}"
case Dp0(bnd, bod):
return f"+[{show(bnd, vars, subs)} {show(bod, vars, subs)}]"
case Dp1(bod, bnd):
return f"+[{show(bod, vars, subs)} {show(bnd, vars, subs)}]"
def wire() -> tuple[Pos, Neg]:
x = next(name)
return Var(x), Sub(x)
type Rdx = tuple[Neg, Pos]
def reduce(book: set[Rdx], vars: dict[Name, Pos], subs: dict[Name, Neg]) -> int:
itrs = 0
while book:
itrs += 1
match book.pop():
case lhs, Var(nam) if nam in vars:
book.add((lhs, vars.pop(nam)))
case lhs, Var(nam):
subs[nam] = lhs
case Sub(nam), rhs if nam in subs:
book.add((subs.pop(nam), rhs))
case Sub(nam), rhs:
vars[nam] = rhs
case Era(), Nil():
pass
case Era(), Lam(bnd, bod):
book.add((bnd, Nil()))
book.add((Era(), bod))
case Era(), Sup(spl, sp0, sp1):
book.add((Era(), sp0))
book.add((Era(), sp1))
case Era(), Usp(us0, us1):
book.add((Era(), us0))
book.add((Era(), us1))
case Era(), Dp0(bnd, bod):
book.add((bnd, bod))
case Era(), Dp1(bod, bnd):
book.add((bnd, bod))
case App(arg, ret), Nil():
book.add((Era(), arg))
book.add((ret, Nil()))
case App(arg, ret), Lam(bnd, bod):
book.add((bnd, arg))
book.add((ret, bod))
case App(arg, ret), Sup(spl, sp0, sp1):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((Dup(spl, an, bn), arg))
book.add((ret, Sup(spl, cp, dp)))
book.add((App(ap, cn), sp0))
book.add((App(bp, dn), sp1))
case App(arg, ret), Usp(us0, us1):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
lab = next(label)
book.add((Dup(lab, an, bn), arg))
book.add((ret, Sup(lab, cp, dp)))
book.add((App(ap, cn), us0))
book.add((App(bp, dn), us1))
case App(arg, ret), Dp0(bnd, bod):
book.add((bnd, Dp1(bod, App(arg, ret))))
case App(arg, ret), Dp1(bod, bnd):
book.add((Udp(bnd, App(arg, ret)), bod))
case Dup(dpl, dp0, dp1), Nil():
book.add((dp0, Nil()))
book.add((dp1, Nil()))
case Dup(dpl, dp0, dp1), Lam(bnd, bod):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((dp0, Lam(an, bp)))
book.add((dp1, Lam(cn, dp)))
book.add((bnd, Sup(dpl, ap, cp)))
book.add((Dup(dpl, bn, dn), bod))
case Dup(dpl, dp0, dp1), Sup(spl, sp0, sp1) if dpl == spl:
book.add((dp0, sp0))
book.add((dp1, sp1))
case Dup(dpl, dp0, dp1), Sup(spl, sp0, sp1):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((dp0, Sup(spl, ap, bp)))
book.add((dp1, Sup(spl, cp, dp)))
book.add((Dup(dpl, an, cn), sp0))
book.add((Dup(dpl, bn, dn), sp1))
case Dup(dpl, dp0, dp1), Usp(us0, us1):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((dp0, Usp(ap, bp)))
book.add((dp1, Usp(cp, dp)))
book.add((Dup(dpl, an, cn), us0))
book.add((Dup(dpl, bn, dn), us1))
case Dup(dpl, dp0, dp1), Dp0(bnd, bod):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((dp0, Dp0(an, bp)))
book.add((dp1, Dp0(cn, dp)))
book.add((bnd, Sup(dpl, ap, cp)))
book.add((Dup(dpl, bn, dn), bod))
case Dup(dpl, dp0, dp1), Dp1(bod, bnd):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((dp0, Dp1(ap, bn)))
book.add((dp1, Dp1(cp, dn)))
book.add((Dup(dpl, an, cn), bod))
book.add((bnd, Sup(dpl, bp, dp)))
case Udp(ud0, ud1), Nil():
book.add((ud0, Nil()))
book.add((ud1, Nil()))
case Udp(ud0, ud1), Lam(bnd, bod):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
lab = next(label)
book.add((ud0, Lam(an, bp)))
book.add((ud1, Lam(cn, dp)))
book.add((bnd, Sup(lab, ap, cp)))
book.add((Dup(lab, bn, dn), bod))
case Udp(ud0, ud1), Sup(spl, sp0, sp1):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((ud0, Sup(spl, ap, bp)))
book.add((ud1, Sup(spl, cp, dp)))
book.add((Udp(an, cn), sp0))
book.add((Udp(bn, dn), sp1))
case Udp(ud0, ud1), Usp(us0, us1):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((ud0, Usp(ap, bp)))
book.add((ud1, Usp(cp, dp)))
book.add((Udp(an, cn), us0))
book.add((Udp(bn, dn), us1))
case Udp(ud0, ud1), Dp0(bnd, bod):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((ud0, Dp0(an, bp)))
book.add((ud1, Dp0(cn, dp)))
book.add((bnd, Usp(ap, cp)))
book.add((Udp(bn, dn), bod))
case Udp(ud0, ud1), Dp1(bod, bnd):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((ud0, Dp1(ap, bn)))
book.add((ud1, Dp1(cp, dn)))
book.add((Udp(an, cn), bod))
book.add((bnd, Usp(bp, dp)))
return itrs
def print_state(root: Term, book: set[Rdx], vars: dict[Name, Pos], subs: dict[Name, Neg]) -> None:
print("ROOT:")
print(f" {show(root, vars, subs)}")
print()
print("BOOK:")
for lhs, rhs in book:
print(f" {show(lhs, vars, subs)} ⋈ {show(rhs, vars, subs)}")
def print_reduction(root: Term, book: set[Rdx]) -> None:
vars: dict[Name, Pos] = {}
subs: dict[Name, Neg] = {}
print("=" * 30)
print("=", "ORIG".center(26), "=")
print("=" * 30)
print()
print_state(root, book, vars, subs)
print()
print("=" * 30)
print("=", "REDUCED".center(26), "=")
print("=" * 30)
print()
itrs = reduce(book, vars, subs)
print_state(root, book, vars, subs)
print()
print(f"ITRS: {itrs}")
def mk_app(book: set[Rdx], fun: Pos, arg: Pos) -> Pos:
rp, rn = wire()
book.add((App(arg, rn), fun))
return rp
def mk_udp(book: set[Rdx], x: Pos) -> tuple[Pos, Pos]:
x0p, x0n = wire()
x1p, x1n = wire()
book.add((Udp(x0n, x1n), x))
return x0p, x1p
def mk_dp0(x: Pos) -> tuple[Pos, Pos]:
x1p, x1n = wire()
return Dp0(x1n, x), x1p
def mk_c2(book: set[Rdx]) -> Pos:
f0p, f0n = wire()
f1p, f1n = wire()
xp, xn = wire()
fx = mk_app(book, f1p, xp)
ffx = mk_app(book, f0p, fx)
return Lam(Udp(f0n, f1n), Lam(xn, ffx))
def mk_cpow2(book: set[Rdx], k: int) -> Pos:
# k=1 -> c2, k=2 -> c4, k=3 -> c8, ...
# c_{2^k} = λf. c2 (c_{2^(k-1)} f)
if k < 1:
raise ValueError("k must be >= 1")
if k == 1:
return mk_c2(book)
fp, fn = wire()
prev = mk_cpow2(book, k - 1) # c_{2^(k-1)}
prev_f = mk_app(book, prev, fp) # f^(2^(k-1))
body = mk_app(book, mk_c2(book), prev_f) # square -> f^(2^k)
return Lam(fn, body)
# λt.λf.t
def mk_true() -> Pos:
tp, tn = wire()
return Lam(tn, Lam(Era(), tp))
# λt.λf.f
def mk_false() -> Pos:
fp, fn = wire()
return Lam(Era(), Lam(fn, fp))
# λb.λt.λf.(b f f)
def mk_clr() -> Pos:
fp, fn = wire()
f1p, f1n = wire()
rp, rn = wire()
return Lam(App(Dp0(f1n, fp), App(f1p, rn)), Lam(Era(), Lam(fn, rp)))
# g = λy.y
# f = λx.(x g g)
# ((f λa.λb.a) (f λc.λd.d))
def test_jamespayor(book: set[Rdx]) -> Pos:
yp, yn = wire()
g0, g1 = mk_dp0(Lam(yn, yp))
xp, xn = wire()
f0, f1 = mk_udp(book, Lam(xn, mk_app(book, mk_app(book, xp, g0), g1)))
ap, an = wire()
dp, dn = wire()
return mk_app(book, mk_app(book, f0, Lam(an, Lam(Era(), ap))), mk_app(book, f1, Lam(Era(), Lam(dn, dp))))
def test_clr_fusion(book: set[Rdx]) -> Pos:
true = mk_true()
false = mk_false()
clr = mk_clr()
N = 100
c_2powN = mk_cpow2(book, N)
clr_2powN = mk_app(book, c_2powN, clr)
# return mk_app(book, clr_2powN, true)
return mk_app(book, clr_2powN, false)
def main() -> None:
book = set[Rdx]()
# root = test_clr_fusion(book)
root = test_jamespayor(book)
print_reduction(root, book)
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment