Skip to content

Instantly share code, notes, and snippets.

@LeeeeT

LeeeeT/ic.py

Created January 5, 2026 05:07
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save LeeeeT/1f7d7717f5a8316c287e7472602c0065 to your computer and use it in GitHub Desktop.
Download ZIP
k-SIC + DUP rotations
Raw
ic.py
import itertools
from dataclasses import dataclass
type Name = int
name = itertools.count()
type Label = int
label = itertools.count()
type Pos = Var | Nil | Lam | Sup | Dp0 | Dp1
type Neg = Sub | Era | App | Dup
@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 Dp0:
d0l: Label
bnd: Neg
bod: Pos
@dataclass(frozen=True)
class Dp1:
d1l: Label
bod: Pos
bnd: Neg
def show_pos(pos: Pos) -> str:
match pos:
case Var(nam):
return f"+{nam}"
case Nil():
return "+_"
case Lam(bnd, bod):
return f"+({show_neg(bnd)} {show_pos(bod)})"
case Sup(spl, sp0, sp1):
return f"+&{spl}{{{show_pos(sp0)} {show_pos(sp1)}}}"
case Dp0(d0l, bnd, bod):
return f"+&{d0l}[{show_neg(bnd)} {show_pos(bod)}]"
case Dp1(d1l, bod, bnd):
return f"+&{d1l}[{show_pos(bod)} {show_neg(bnd)}]"
def show_neg(neg: Neg) -> str:
match neg:
case Sub(nam):
return f"-{nam}"
case Era():
return "-_"
case App(arg, ret):
return f"-({show_pos(arg)} {show_neg(ret)})"
case Dup(dpl, dp0, dp1):
return f"-&{dpl}{{{show_neg(dp0)} {show_neg(dp1)}}}"
def resolve_pos(pos: Pos, vars: dict[Name, Pos], subs: dict[Name, Neg]) -> Pos:
match pos:
case Var(nam) if nam in vars:
return resolve_pos(vars[nam], vars, subs)
case Var(nam):
return Var(nam)
case Nil():
return Nil()
case Lam(bnd, bod):
return Lam(resolve_neg(bnd, vars, subs), resolve_pos(bod, vars, subs))
case Sup(spl, sp0, sp1):
return Sup(spl, resolve_pos(sp0, vars, subs), resolve_pos(sp1, vars, subs))
case Dp0(d0l, bnd, bod):
return Dp0(d0l, resolve_neg(bnd, vars, subs), resolve_pos(bod, vars, subs))
case Dp1(d1l, bod, bnd):
return Dp1(d1l, resolve_pos(bod, vars, subs), resolve_neg(bnd, vars, subs))
def resolve_neg(neg: Neg, vars: dict[Name, Pos], subs: dict[Name, Neg]) -> Neg:
match neg:
case Sub(nam) if nam in subs:
return resolve_neg(subs[nam], vars, subs)
case Sub(nam):
return Sub(nam)
case Era():
return Era()
case App(arg, ret):
return App(resolve_pos(arg, vars, subs), resolve_neg(ret, vars, subs))
case Dup(dpl, dp0, dp1):
return Dup(dpl, resolve_neg(dp0, vars, subs), resolve_neg(dp1, 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(), Dp0(d0l, bnd, bod):
book.add((bnd, bod))
case Era(), Dp1(d1l, 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), Dp0(d0l, bnd, bod):
book.add((bnd, Dp1(d0l, bod, App(arg, ret))))
case App(arg, ret), Dp1(d1l, bod, bnd):
book.add((Dup(d1l, 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), Dp0(d0l, bnd, bod) if dpl == d0l:
book.add((Dup(dpl, Dup(dpl, dp0, dp1), bnd), bod))
case Dup(dpl, dp0, dp1), Dp0(d0l, bnd, bod):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((dp0, Dp0(d0l, an, bp)))
book.add((dp1, Dp0(d0l, cn, dp)))
book.add((bnd, Sup(dpl, ap, cp)))
book.add((Dup(dpl, bn, dn), bod))
case Dup(dpl, dp0, dp1), Dp1(d1l, bod, bnd) if dpl == d1l:
book.add((Dup(dpl, bnd, Dup(dpl, dp0, dp1)), bod))
case Dup(dpl, dp0, dp1), Dp1(d1l, bod, bnd):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((dp0, Dp1(d1l, ap, bn)))
book.add((dp1, Dp1(d1l, cp, dn)))
book.add((Dup(dpl, an, cn), bod))
book.add((bnd, Sup(dpl, bp, dp)))
return itrs
def print_state(root: Pos, book: set[Rdx]) -> None:
print("ROOT:")
print(f" {show_pos(root)}")
print()
print("BOOK:")
for lhs, rhs in book:
print(f" {show_neg(lhs)} ⋈ {show_pos(rhs)}")
def print_reduction(root: Pos, 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)
print()
print("=" * 30)
print("=", "REDUCED".center(26), "=")
print("=" * 30)
print()
itrs = reduce(book, vars, subs)
resolved = resolve_pos(root, vars, subs)
print_state(resolved, book)
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_dup(book: set[Rdx], x: Pos, lab: Label | None = None) -> tuple[Pos, Pos]:
if lab is None:
lab = next(label)
x0p, x0n = wire()
x1p, x1n = wire()
book.add((Dup(lab, x0n, x1n), x))
return x0p, x1p
def mk_dp0(x: Pos, lab: Label | None = None) -> tuple[Pos, Pos]:
if lab is None:
lab = next(label)
x1p, x1n = wire()
return Dp0(lab, x1n, x), x1p
def mk_c2(book: set[Rdx]) -> Pos:
l = next(label)
f0p, f0n = wire()
f1p, f1n = wire()
xp, xn = wire()
fx = mk_app(book, f1p, xp)
ffx = mk_app(book, f0p, fx)
return Lam(Dup(l, 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:
l = next(label)
fp, fn = wire()
f1p, f1n = wire()
rp, rn = wire()
return Lam(App(Dp0(l, 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_dup(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