Skip to content

Instantly share code, notes, and snippets.

@LeeeeT

LeeeeT/sic.py

Last active January 14, 2026 10:44
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save LeeeeT/26dcfd2d7cdca271a70561fc9375fb0f to your computer and use it in GitHub Desktop.
Download ZIP
k-SIC + universal δ + McCarthy's amb
Raw
sic.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 | Usp | Cob
type Neg = Sub | Era | App | Dup | Udp | Amb
@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:
ud0: Name
ud1: Name
@dataclass(frozen=True)
class Usp:
us0: Name
us1: Name
@dataclass(frozen=True)
class Amb:
m: Name
a: Name
@dataclass(frozen=True)
class Cob:
m: Name
a: 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, ud0: Name, ud1: Name) -> Name:
udp = next(name)
net.subs[udp] = Udp(ud0, ud1)
return udp
def usp(net: Net, us0: Name, us1: Name) -> Name:
usp = next(name)
net.vars[usp] = Usp(us0, us1)
return usp
def amb(net: Net, m: Name, a: Name) -> Name:
amb = next(name)
net.subs[amb] = Amb(m, a)
return amb
def cob(net: Net, m: Name, a: Name) -> Name:
cob = next(name)
net.vars[cob] = Cob(m, a)
return cob
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 Var(nam):
return f"+{nam}"
case Nil():
return "+_"
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 Usp(us0, us1):
return f"+{{{show_pos(net, us0)} {show_pos(net, us1)}}}"
case Cob(cb0, cb1):
return f"+[{show_pos(net, cb0)} {show_pos(net, cb1)}]"
def show_neg(net: Net, neg: Name) -> str:
match net.subs[neg]:
case Sub(nam):
return f"-{nam}"
case Era():
return "-_"
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 Udp(ud0, ud1):
return f"-{{{show_neg(net, ud0)} {show_neg(net, ud1)}}}"
case Amb(am0, am1):
return f"-[{show_neg(net, am0)} {show_neg(net, am1)}]"
def resolve_pos(net: Net, pos: Name) -> None:
match net.vars[pos]:
case Var(nam) if nam in net.vars:
resolve_pos(net, nam)
net.vars[pos] = net.vars.pop(nam)
case Var(nam):
pass
case Nil():
pass
case Lam(bnd, bod):
resolve_neg(net, bnd)
resolve_pos(net, bod)
case Sup(spl, sp0, sp1):
resolve_pos(net, sp0)
resolve_pos(net, sp1)
case Usp(us0, us1):
resolve_pos(net, us0)
resolve_pos(net, us1)
case Cob(cb0, cb1):
resolve_pos(net, cb0)
resolve_pos(net, cb1)
def resolve_neg(net: Net, neg: Name) -> None:
match net.subs[neg]:
case Sub(nam) if nam in net.subs:
resolve_neg(net, nam)
net.subs[neg] = net.subs.pop(nam)
case Sub(nam):
pass
case Era():
pass
case App(arg, ret):
resolve_pos(net, arg)
resolve_neg(net, ret)
case Dup(dpl, dp0, dp1):
resolve_neg(net, dp0)
resolve_neg(net, dp1)
case Udp(ud0, ud1):
resolve_neg(net, ud0)
resolve_neg(net, ud1)
case Amb(am0, am1):
resolve_neg(net, am0)
resolve_neg(net, am1)
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):
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:
net.vars[nam] = rhsc
case lhsc, Cob(m, a) if m in net.vars:
net.subs[lhs] = lhsc
x = next(name)
net.vars[x] = net.vars.pop(m)
net.book.add((lhs, x))
case lhsc, Cob(m, a):
net.subs[lhs] = lhsc
net.book.add((lhs, a))
case Amb(m, a), rhsc if m in net.subs:
net.vars[rhs] = rhsc
x = next(name)
net.subs[x] = net.subs.pop(m)
net.book.add((x, rhs))
case Amb(m, a), rhsc:
net.vars[rhs] = rhsc
net.book.add((a, rhs))
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(), Usp(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), Usp(us0, us1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
lab = next(label)
net.book.add((dup(net, lab, an, bn), arg))
net.book.add((ret, sup(net, lab, cp, dp)))
net.book.add((app(net, ap, cn), us0))
net.book.add((app(net, bp, dn), us1))
case Dup(dpl, 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), Usp(us0, us1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((dp0, usp(net, ap, bp)))
net.book.add((dp1, usp(net, cp, dp)))
net.book.add((dup(net, dpl, an, cn), us0))
net.book.add((dup(net, dpl, bn, dn), us1))
case Udp(ud0, ud1), Nil():
net.book.add((ud0, nil(net)))
net.book.add((ud1, nil(net)))
case Udp(ud0, ud1), Lam(bnd, bod):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
lab = next(label)
net.book.add((ud0, lam(net, an, bp)))
net.book.add((ud1, lam(net, cn, dp)))
net.book.add((bnd, sup(net, lab, ap, cp)))
net.book.add((dup(net, lab, bn, dn), bod))
case Udp(ud0, ud1), Sup(spl, sp0, sp1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((ud0, sup(net, spl, ap, bp)))
net.book.add((ud1, sup(net, spl, cp, dp)))
net.book.add((udp(net, an, cn), sp0))
net.book.add((udp(net, bn, dn), sp1))
case Udp(ud0, ud1), Usp(us0, us1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((ud0, usp(net, ap, bp)))
net.book.add((ud1, usp(net, cp, dp)))
net.book.add((udp(net, an, cn), us0))
net.book.add((udp(net, bn, dn), 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)
resolve_pos(net, root)
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]:
x0p, x0n = wire(net)
x1p, x1n = wire(net)
net.book.add((udp(net, x0n, x1n), x))
return x0p, x1p
def mk_amb(net: Net, fst: Name, snd: Name) -> tuple[Name, Name]:
xp, xn = wire(net)
yp, yn = wire(net)
net.book.add((amb(net, xn, yn), fst))
net.book.add((amb(net, xn, yn), snd))
return xp, yp
# λ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.(b true false)
def mk_bool_eta_expand(net: Net) -> Name:
bp, bn = wire(net)
return lam(net, bn, mk_app(net, mk_app(net, bp, mk_true(net)), mk_false(net)))
# λa.λb.λt.λf.(a t (b t f))
def mk_or(net: Net) -> Name:
ap, an = wire(net)
bp, bn = wire(net)
tp, tn = wire(net)
fp, fn = wire(net)
t0, t1 = mk_udp(net, tp)
at = mk_app(net, ap, t0)
btf = mk_app(net, mk_app(net, bp, t1), fp)
ret = mk_app(net, at, btf)
return lam(net, an, lam(net, bn, lam(net, tn, lam(net, fn, ret))))
# parallel or
# λa.λb. (x,y)=amb(a,b); (or x y)
def mk_por(net: Net) -> Name:
ap, an = wire(net)
bp, bn = wire(net)
x, y = mk_amb(net, ap, bp)
ret = mk_app(net, mk_app(net, mk_or(net), x), y)
return lam(net, an, lam(net, bn, ret))
# A or TRUE, where A is stuck
# {a0,a1}=a0; (or a1 true)
def mk_test_or(net: Net) -> Name:
a0p, a0n = wire(net)
a1p, a1n = wire(net)
net.book.add((udp(net, a0n, a1n), a0p))
return mk_app(net, mk_app(net, mk_or(net), a1p), mk_true(net))
# A por TRUE, where A is stuck
# {a0,a1}=a0; (por a1 true)
def mk_test_por(net: Net) -> Name:
a0p, a0n = wire(net)
a1p, a1n = wire(net)
net.book.add((udp(net, a0n, a1n), a0p))
return mk_app(net, mk_app(net, mk_por(net), a1p), mk_true(net))
def main() -> None:
net = empty_net()
# root = mk_app(net, mk_bool_eta_expand(net), mk_test_or(net)) # expect a dangling wire
root = mk_app(net, mk_bool_eta_expand(net), mk_test_por(net)) # expect TRUE
print_reduction(net, root)
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment