Skip to content

Instantly share code, notes, and snippets.

@LeeeeT

LeeeeT/gc.py

Last active January 31, 2026 23:57
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save LeeeeT/2736ee2b4f3661c0eb1ea4d981dd063c to your computer and use it in GitHub Desktop.
Download ZIP
k-SIC + Opportunistic Swap
Raw
gc.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 | Udp | Usl
type Neg = Sub | Era | App | Dup | Usp | Udl
@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: Name
bod: Name
@dataclass(frozen=True)
class App:
arg: Name
ret: Name
@dataclass(frozen=True)
class Dup:
dpl: Label
dp0: Name
dp1: Name
@dataclass(frozen=True)
class Sup:
spl: Label
sp0: Name
sp1: Name
@dataclass(frozen=True)
class Udp:
udb: Name
@dataclass(frozen=True)
class Usp:
usb: Name
@dataclass(frozen=True)
class Udl:
ud0: Name
ud1: Name
@dataclass(frozen=True)
class Usl:
us0: Name
us1: Name
type Rdx = tuple[Name, Name]
@dataclass(frozen=True)
class Net:
book: set[Rdx]
vars: dict[Name, Pos]
subs: dict[Name, Neg]
def empty_net() -> Net:
return Net(set(), {}, {})
def var(net: Net, nam: Name) -> Name:
var = next(name)
net.vars[var] = Var(nam)
return var
def sub(net: Net, nam: Name) -> Name:
sub = next(name)
net.subs[sub] = Sub(nam)
return sub
def nil(net: Net) -> Name:
nil = next(name)
net.vars[nil] = Nil()
return nil
def era(net: Net) -> Name:
era = next(name)
net.subs[era] = Era()
return era
def lam(net: Net, bnd: Name, bod: Name) -> Name:
lam = next(name)
net.vars[lam] = Lam(bnd, bod)
return lam
def app(net: Net, arg: Name, ret: Name) -> Name:
app = next(name)
net.subs[app] = App(arg, ret)
return app
def dup(net: Net, dpl: Label, dp0: Name, dp1: Name) -> Name:
dup = next(name)
net.subs[dup] = Dup(dpl, dp0, dp1)
return dup
def sup(net: Net, spl: Label, sp0: Name, sp1: Name) -> Name:
sup = next(name)
net.vars[sup] = Sup(spl, sp0, sp1)
return sup
def udp(net: Net, udb: Name) -> Name:
udp = next(name)
net.vars[udp] = Udp(udb)
return udp
def usp(net: Net, usb: Name) -> Name:
usp = next(name)
net.subs[usp] = Usp(usb)
return usp
def udl(net: Net, ud0: Name, ud1: Name) -> Name:
udl = next(name)
net.subs[udl] = Udl(ud0, ud1)
return udl
def usl(net: Net, us0: Name, us1: Name) -> Name:
usl = next(name)
net.vars[usl] = Usl(us0, us1)
return usl
def wire(net: Net) -> tuple[Name, Name]:
nam = next(name)
return var(net, nam), sub(net, nam)
def show_pos(net: Net, pos: Name) -> str:
match net.vars[pos]:
case Nil():
return "+_"
case Var(nam) if nam in net.vars:
return show_pos(net, nam)
case Var(nam):
return f"+{nam}"
case Lam(bnd, bod):
return f"+({show_neg(net, bnd)} {show_pos(net, bod)})"
case Sup(spl, sp0, sp1):
return f"+&{spl}{{{show_pos(net, sp0)} {show_pos(net, sp1)}}}"
case Udp(udb):
# return f"+{{{show_pos(net, udb)}}}"
return show_pos(net, udb)
case Usl(us0, us1):
return f"+{{{show_pos(net, us0)} {show_pos(net, us1)}}}"
def show_neg(net: Net, neg: Name) -> str:
match net.subs[neg]:
case Era():
return "_-"
case Sub(nam) if nam in net.subs:
return show_neg(net, nam)
case Sub(nam):
return f"-{nam}"
case App(arg, ret):
return f"-({show_pos(net, arg)} {show_neg(net, ret)})"
case Dup(dpl, dp0, dp1):
return f"-&{dpl}{{{show_neg(net, dp0)} {show_neg(net, dp1)}}}"
case Usp(usb):
# return f"+{{{show_neg(net, usb)}}}"
return show_neg(net, usb)
case Udl(ud0, ud1):
return f"+{{{show_neg(net, ud0)} {show_neg(net, ud1)}}}"
def reduce(net: Net) -> int:
itrs = 0
while net.book:
itrs += 1
lhs, rhs = net.book.pop()
match net.subs.pop(lhs), net.vars.pop(rhs):
case lhsc, Var(nam) if nam in net.vars:
net.subs[lhs] = lhsc
net.book.add((lhs, nam))
case lhsc, Var(nam):
if isinstance(lhsc, Usp):
net.subs[lhs] = Sub(nam)
net.subs[nam] = lhsc
case Sub(nam), rhsc if nam in net.subs:
net.vars[rhs] = rhsc
net.book.add((nam, rhs))
case Sub(nam), rhsc:
if isinstance(rhsc, Udp):
net.vars[rhs] = Var(nam)
net.vars[nam] = rhsc
case Usp(usb), Nil():
net.subs[lhs] = Sub(usb)
case Usp(usb), Usl(us0, us1):
ap, an = wire(net)
net.book.add((usb, usl(net, us0, ap)))
usp0 = usp(net, an)
net.book.add((usp0, us1))
net.subs[lhs] = Sub(usp0)
case Usp(usb), rhsc:
ap, an = wire(net)
net.vars[rhs] = rhsc
net.book.add((usb, usl(net, rhs, ap)))
net.subs[lhs] = net.subs.pop(an)
case Era(), Udp(udb):
net.vars[rhs] = Var(udb)
case Udl(ud0, ud1), Udp(udb):
ap, an = wire(net)
net.book.add((udl(net, ud0, an), udb))
udp0 = udp(net, ap)
net.book.add((ud1, udp0))
net.vars[rhs] = Var(udp0)
case lhsc, Udp(udb):
ap, an = wire(net)
net.subs[lhs] = lhsc
net.book.add((udl(net, lhs, an), udb))
net.vars[rhs] = net.vars.pop(ap)
case Era(), Nil():
pass
case Era(), Lam(bnd, bod):
net.book.add((bnd, nil(net)))
net.book.add((era(net), bod))
case Era(), Sup(spl, sp0, sp1):
net.book.add((era(net), sp0))
net.book.add((era(net), sp1))
case Era(), Usl(us0, us1):
net.book.add((era(net), us0))
net.book.add((era(net), us1))
case App(arg, ret), Nil():
net.book.add((era(net), arg))
net.book.add((ret, nil(net)))
case App(arg, ret), Lam(bnd, bod):
net.book.add((bnd, arg))
net.book.add((ret, bod))
case App(arg, ret), Sup(spl, sp0, sp1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((dup(net, spl, an, bn), arg))
net.book.add((ret, sup(net, spl, cp, dp)))
net.book.add((app(net, ap, cn), sp0))
net.book.add((app(net, bp, dn), sp1))
case App(arg, ret), Usl(us0, us1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
udp0 = udp(net, arg)
usp0 = usp(net, ret)
net.book.add((app(net, udp0, usp0), us0))
net.book.add((app(net, udp0, usp0), us1))
case Dup(dp0, dp1), Nil():
net.book.add((dp0, nil(net)))
net.book.add((dp1, nil(net)))
case Dup(dpl, dp0, dp1), Lam(bnd, bod):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((dp0, lam(net, an, bp)))
net.book.add((dp1, lam(net, cn, dp)))
net.book.add((bnd, sup(net, dpl, ap, cp)))
net.book.add((dup(net, dpl, bn, dn), bod))
case Dup(dpl, dp0, dp1), Sup(spl, sp0, sp1) if dpl == spl:
net.book.add((dp0, sp0))
net.book.add((dp1, sp1))
case Dup(dpl, dp0, dp1), Sup(spl, sp0, sp1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((dp0, sup(net, spl, ap, bp)))
net.book.add((dp1, sup(net, spl, cp, dp)))
net.book.add((dup(net, dpl, an, cn), sp0))
net.book.add((dup(net, dpl, bn, dn), sp1))
case Dup(dpl, dp0, dp1), Usl(us0, us1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
usp0 = udp(net, dp0)
usp1 = usp(net, dp1)
net.book.add((dup(net, dpl, usp0, usp1), us0))
net.book.add((dup(net, dpl, usp0, usp1), us1))
case Udl(ud0, ud1), Nil():
net.book.add((ud0, nil(net)))
net.book.add((ud1, nil(net)))
case Udl(ud0, ud1), Lam(bnd, bod):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
usp0 = usp(net, bnd)
udp0 = udp(net, bod)
net.book.add((ud0, lam(net, usp0, udp0)))
net.book.add((ud1, lam(net, usp0, udp0)))
case Udl(ud0, ud1), Sup(spl, sp0, sp1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
udp0 = udp(net, sp0)
udp1 = udp(net, sp1)
net.book.add((ud0, sup(net, spl, udp0, udp1)))
net.book.add((ud1, sup(net, spl, udp0, udp1)))
case Udl(ud0, ud1), Usl(us0, us1):
net.book.add((ud0, us0))
net.book.add((ud1, us1))
case _:
raise RuntimeError
return itrs
def print_state(net: Net, root: Name, *, heap: bool = False) -> None:
print("ROOT:")
print(f" {show_pos(net, root)}")
print()
print("BOOK:")
for lhs, rhs in net.book:
print(f" {show_neg(net, lhs)} ⋈ {show_pos(net, rhs)}")
if heap:
print()
print("VARS:")
for nam in net.vars:
print(f" {nam} = {show_pos(net, nam)}")
print()
print("SUBS:")
for nam in net.subs:
print(f" {nam} = {show_neg(net, nam)}")
def print_reduction(net: Net, root: Name, *, heap: bool = False) -> None:
print("=" * 30)
print("=", "INITIAL".center(26), "=")
print("=" * 30)
print()
print_state(net, root, heap=heap)
print()
print("=" * 30)
print("=", "NORMALIZED".center(26), "=")
print("=" * 30)
print()
itrs = reduce(net)
print_state(net, root, heap=heap)
print()
print(f"ITRS: {itrs}")
def mk_app(net: Net, fun: Name, arg: Name) -> Name:
rp, rn = wire(net)
net.book.add((app(net, arg, rn), fun))
return rp
def mk_dup(net: Net, x: Name, lab: Label | None = None) -> tuple[Name, Name]:
if lab is None:
lab = next(label)
x0p, x0n = wire(net)
x1p, x1n = wire(net)
net.book.add((dup(net, lab, x0n, x1n), x))
return x0p, x1p
def mk_udp(net: Net, x: Name) -> tuple[Name, Name]:
udp0 = udp(net, x)
return udp0, udp0
def mk_c2(net: Net) -> Name:
f0p, f0n = wire(net)
f1p, f1n = wire(net)
xp, xn = wire(net)
fx = mk_app(net, f1p, xp)
ffx = mk_app(net, f0p, fx)
return lam(net, dup(net, next(label), f0n, f1n), lam(net, xn, ffx))
def mk_cpow2(net: Net, k: int) -> Name:
# 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(net)
fp, fn = wire(net)
prev = mk_cpow2(net, k - 1) # c_{2^(k-1)}
prev_f = mk_app(net, prev, fp) # f^(2^(k-1))
body = mk_app(net, mk_c2(net), prev_f) # square -> f^(2^k)
return lam(net, fn, body)
# λt.λf.t
def mk_true(net: Net) -> Name:
tp, tn = wire(net)
return lam(net, tn, lam(net, era(net), tp))
# λt.λf.f
def mk_false(net: Net) -> Name:
fp, fn = wire(net)
return lam(net, era(net), lam(net, fn, fp))
# λb.λt.λf.(b f f)
def mk_clr(net: Net) -> Name:
bp, bn = wire(net)
fp, fn = wire(net)
f0, f1 = mk_udp(net, fp)
return lam(net, bn, lam(net, era(net), lam(net, fn, mk_app(net, mk_app(net, bp, f0), f1))))
# g = λy.y
# f = λx.(x g g)
# ((f λa.λb.a) (f λc.λd.d))
def test_jamespayor(net: Net) -> Name:
yp, yn = wire(net)
g0, g1 = mk_udp(net, lam(net, yn, yp))
xp, xn = wire(net)
f0, f1 = mk_dup(net, lam(net, xn, mk_app(net, mk_app(net, xp, g0), g1)))
ap, an = wire(net)
dp, dn = wire(net)
return mk_app(net, mk_app(net, f0, lam(net, an, lam(net, era(net), ap))), mk_app(net, f1, lam(net, era(net), lam(net, dn, dp))))
# (clr^N true)
def test_clr_fusion(net: Net, N: int) -> Name:
return mk_app(net, mk_app(net, mk_cpow2(net, N), mk_clr(net)), mk_true(net))
def main() -> None:
net = empty_net()
# root = test_jamespayor(net)
root = mk_app(net, mk_cpow2(net, 100), mk_clr(net))
print_reduction(net, root)
main()
Raw
no gc.py
import itertools
from dataclasses import dataclass
type Name = int
name = itertools.count()
type Label = int
label = itertools.count()
type Pos = Var | Lam | Sup | Udp | Usl
type Neg = Sub | App | Dup | Usp | Udl
@dataclass(frozen=True)
class Var:
nam: Name
@dataclass(frozen=True)
class Sub:
nam: Name
@dataclass(frozen=True)
class Lam:
bnd: Name
bod: Name
@dataclass(frozen=True)
class App:
arg: Name
ret: Name
@dataclass(frozen=True)
class Dup:
dpl: Label
dp0: Name
dp1: Name
@dataclass(frozen=True)
class Sup:
spl: Label
sp0: Name
sp1: Name
@dataclass(frozen=True)
class Udp:
udb: Name
@dataclass(frozen=True)
class Usp:
usb: Name
@dataclass(frozen=True)
class Udl:
ud0: Name
ud1: Name
@dataclass(frozen=True)
class Usl:
us0: Name
us1: Name
type Rdx = tuple[Name, Name]
@dataclass(frozen=True)
class Net:
book: set[Rdx]
vars: dict[Name, Pos]
subs: dict[Name, Neg]
def empty_net() -> Net:
return Net(set(), {}, {})
def var(net: Net, nam: Name) -> Name:
var = next(name)
net.vars[var] = Var(nam)
return var
def sub(net: Net, nam: Name) -> Name:
sub = next(name)
net.subs[sub] = Sub(nam)
return sub
def lam(net: Net, bnd: Name, bod: Name) -> Name:
lam = next(name)
net.vars[lam] = Lam(bnd, bod)
return lam
def app(net: Net, arg: Name, ret: Name) -> Name:
app = next(name)
net.subs[app] = App(arg, ret)
return app
def dup(net: Net, dpl: Label, dp0: Name, dp1: Name) -> Name:
dup = next(name)
net.subs[dup] = Dup(dpl, dp0, dp1)
return dup
def sup(net: Net, spl: Label, sp0: Name, sp1: Name) -> Name:
sup = next(name)
net.vars[sup] = Sup(spl, sp0, sp1)
return sup
def udp(net: Net, udb: Name) -> Name:
udp = next(name)
net.vars[udp] = Udp(udb)
return udp
def usp(net: Net, usb: Name) -> Name:
usp = next(name)
net.subs[usp] = Usp(usb)
return usp
def udl(net: Net, ud0: Name, ud1: Name) -> Name:
udl = next(name)
net.subs[udl] = Udl(ud0, ud1)
return udl
def usl(net: Net, us0: Name, us1: Name) -> Name:
usl = next(name)
net.vars[usl] = Usl(us0, us1)
return usl
def wire(net: Net) -> tuple[Name, Name]:
nam = next(name)
return var(net, nam), sub(net, nam)
def show_pos(net: Net, pos: Name) -> str:
match net.vars.get(pos):
case None:
return "+_"
case Var(nam) if nam in net.vars:
return show_pos(net, nam)
case Var(nam):
return f"+{nam}"
case Lam(bnd, bod):
return f"+({show_neg(net, bnd)} {show_pos(net, bod)})"
case Sup(spl, sp0, sp1):
return f"+&{spl}{{{show_pos(net, sp0)} {show_pos(net, sp1)}}}"
case Udp(udb):
# return f"+{{{show_pos(net, udb)}}}"
return show_pos(net, udb)
case Usl(us0, us1):
return f"+{{{show_pos(net, us0)} {show_pos(net, us1)}}}"
def show_neg(net: Net, neg: Name) -> str:
match net.subs.get(neg):
case None:
return "_-"
case Sub(nam) if nam in net.subs:
return show_neg(net, nam)
case Sub(nam):
return f"-{nam}"
case App(arg, ret):
return f"-({show_pos(net, arg)} {show_neg(net, ret)})"
case Dup(dpl, dp0, dp1):
return f"-&{dpl}{{{show_neg(net, dp0)} {show_neg(net, dp1)}}}"
case Usp(usb):
# return f"+{{{show_neg(net, usb)}}}"
return show_neg(net, usb)
case Udl(ud0, ud1):
return f"+{{{show_neg(net, ud0)} {show_neg(net, ud1)}}}"
def reduce(net: Net) -> int:
itrs = 0
while net.book:
itrs += 1
lhs, rhs = net.book.pop()
match net.subs.pop(lhs), net.vars.pop(rhs):
case lhsc, Var(nam) if nam in net.vars:
net.subs[lhs] = lhsc
net.book.add((lhs, nam))
case lhsc, Var(nam):
if isinstance(lhsc, Usp):
net.subs[lhs] = Sub(nam)
net.subs[nam] = lhsc
case Sub(nam), rhsc if nam in net.subs:
net.vars[rhs] = rhsc
net.book.add((nam, rhs))
case Sub(nam), rhsc:
if isinstance(rhsc, Udp):
net.vars[rhs] = Var(nam)
net.vars[nam] = rhsc
case Usp(usb), Usl(us0, us1):
ap, an = wire(net)
net.book.add((usb, usl(net, us0, ap)))
usp0 = usp(net, an)
net.book.add((usp0, us1))
net.subs[lhs] = Sub(usp0)
case Usp(usb), rhsc:
ap, an = wire(net)
net.vars[rhs] = rhsc
net.book.add((usb, usl(net, rhs, ap)))
net.subs[lhs] = net.subs.pop(an)
case Udl(ud0, ud1), Udp(udb):
ap, an = wire(net)
net.book.add((udl(net, ud0, an), udb))
udp0 = udp(net, ap)
net.book.add((ud1, udp0))
net.vars[rhs] = Var(udp0)
case lhsc, Udp(udb):
ap, an = wire(net)
net.subs[lhs] = lhsc
net.book.add((udl(net, lhs, an), udb))
net.vars[rhs] = net.vars.pop(ap)
case App(arg, ret), Lam(bnd, bod):
net.book.add((bnd, arg))
net.book.add((ret, bod))
case App(arg, ret), Sup(spl, sp0, sp1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((dup(net, spl, an, bn), arg))
net.book.add((ret, sup(net, spl, cp, dp)))
net.book.add((app(net, ap, cn), sp0))
net.book.add((app(net, bp, dn), sp1))
case App(arg, ret), Usl(us0, us1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
udp0 = udp(net, arg)
usp0 = usp(net, ret)
net.book.add((app(net, udp0, usp0), us0))
net.book.add((app(net, udp0, usp0), us1))
case Dup(dpl, dp0, dp1), Lam(bnd, bod):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((dp0, lam(net, an, bp)))
net.book.add((dp1, lam(net, cn, dp)))
net.book.add((bnd, sup(net, dpl, ap, cp)))
net.book.add((dup(net, dpl, bn, dn), bod))
case Dup(dpl, dp0, dp1), Sup(spl, sp0, sp1) if dpl == spl:
net.book.add((dp0, sp0))
net.book.add((dp1, sp1))
case Dup(dpl, dp0, dp1), Sup(spl, sp0, sp1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((dp0, sup(net, spl, ap, bp)))
net.book.add((dp1, sup(net, spl, cp, dp)))
net.book.add((dup(net, dpl, an, cn), sp0))
net.book.add((dup(net, dpl, bn, dn), sp1))
case Dup(dpl, dp0, dp1), Usl(us0, us1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
usp0 = udp(net, dp0)
usp1 = usp(net, dp1)
net.book.add((dup(net, dpl, usp0, usp1), us0))
net.book.add((dup(net, dpl, usp0, usp1), us1))
case Udl(ud0, ud1), Lam(bnd, bod):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
usp0 = usp(net, bnd)
udp0 = udp(net, bod)
net.book.add((ud0, lam(net, usp0, udp0)))
net.book.add((ud1, lam(net, usp0, udp0)))
case Udl(ud0, ud1), Sup(spl, sp0, sp1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
udp0 = udp(net, sp0)
udp1 = udp(net, sp1)
net.book.add((ud0, sup(net, spl, udp0, udp1)))
net.book.add((ud1, sup(net, spl, udp0, udp1)))
case Udl(ud0, ud1), Usl(us0, us1):
net.book.add((ud0, us0))
net.book.add((ud1, us1))
return itrs
def print_state(net: Net, root: Name, *, heap: bool = False) -> None:
print("ROOT:")
print(f" {show_pos(net, root)}")
print()
print("BOOK:")
for lhs, rhs in net.book:
print(f" {show_neg(net, lhs)} ⋈ {show_pos(net, rhs)}")
if heap:
print()
print("VARS:")
for nam in net.vars:
print(f" {nam} = {show_pos(net, nam)}")
print()
print("SUBS:")
for nam in net.subs:
print(f" {nam} = {show_neg(net, nam)}")
def print_reduction(net: Net, root: Name, *, heap: bool = False) -> None:
print("=" * 30)
print("=", "INITIAL".center(26), "=")
print("=" * 30)
print()
print_state(net, root, heap=heap)
print()
print("=" * 30)
print("=", "NORMALIZED".center(26), "=")
print("=" * 30)
print()
itrs = reduce(net)
print_state(net, root, heap=heap)
print()
print(f"ITRS: {itrs}")
def mk_app(net: Net, fun: Name, arg: Name) -> Name:
rp, rn = wire(net)
net.book.add((app(net, arg, rn), fun))
return rp
def mk_dup(net: Net, x: Name, lab: Label | None = None) -> tuple[Name, Name]:
if lab is None:
lab = next(label)
x0p, x0n = wire(net)
x1p, x1n = wire(net)
net.book.add((dup(net, lab, x0n, x1n), x))
return x0p, x1p
def mk_udp(net: Net, x: Name) -> tuple[Name, Name]:
udp0 = udp(net, x)
return udp0, udp0
def mk_c2(net: Net) -> Name:
f0p, f0n = wire(net)
f1p, f1n = wire(net)
xp, xn = wire(net)
fx = mk_app(net, f1p, xp)
ffx = mk_app(net, f0p, fx)
return lam(net, dup(net, next(label), f0n, f1n), lam(net, xn, ffx))
def mk_cpow2(net: Net, k: int) -> Name:
# 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(net)
fp, fn = wire(net)
prev = mk_cpow2(net, k - 1) # c_{2^(k-1)}
prev_f = mk_app(net, prev, fp) # f^(2^(k-1))
body = mk_app(net, mk_c2(net), prev_f) # square -> f^(2^k)
return lam(net, fn, body)
# λt.λf.t
def mk_true(net: Net) -> Name:
tp, tn = wire(net)
fp, fn = wire(net)
return lam(net, tn, lam(net, fn, tp))
# λt.λf.f
def mk_false(net: Net) -> Name:
tp, tn = wire(net)
fp, fn = wire(net)
return lam(net, tn, lam(net, fn, fp))
# λb.λt.λf.(b f f)
def mk_clr(net: Net) -> Name:
bp, bn = wire(net)
tp, tn = wire(net)
fp, fn = wire(net)
f0, f1 = mk_udp(net, fp)
return lam(net, bn, lam(net, tn, lam(net, fn, mk_app(net, mk_app(net, bp, f0), f1))))
# g = λy.y
# f = λx.(x g g)
# ((f λa.λb.a) (f λc.λd.d))
def test_jamespayor(net: Net) -> Name:
yp, yn = wire(net)
g0, g1 = mk_udp(net, lam(net, yn, yp))
xp, xn = wire(net)
f0, f1 = mk_dup(net, lam(net, xn, mk_app(net, mk_app(net, xp, g0), g1)))
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
return mk_app(net, mk_app(net, f0, lam(net, an, lam(net, bn, ap))), mk_app(net, f1, lam(net, cn, lam(net, dn, dp))))
# (clr^N true)
def test_clr_fusion(net: Net, N: int) -> Name:
return mk_app(net, mk_app(net, mk_cpow2(net, N), mk_clr(net)), mk_true(net))
def main() -> None:
net = empty_net()
# root = test_jamespayor(net)
root = test_clr_fusion(net, 100)
print_reduction(net, root)
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment