Skip to content

Instantly share code, notes, and snippets.

@LeeeeT

LeeeeT/explicit_wiring_polarized.py

Last active January 11, 2026 10:35
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save LeeeeT/10b6d079980288223094a57734560865 to your computer and use it in GitHub Desktop.
Download ZIP
SIC cores
Raw
explicit_wiring_polarized.py
import itertools
from dataclasses import dataclass
type Name = int
name = itertools.count()
type Pos = Var | Nil | Lam | Sup
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: Name
bod: Name
@dataclass(frozen=True)
class App:
arg: Name
ret: Name
@dataclass(frozen=True)
class Dup:
dp0: Name
dp1: Name
@dataclass(frozen=True)
class Sup:
sp0: Name
sp1: 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, dp0: Name, dp1: Name) -> Name:
dup = next(name)
net.subs[dup] = Dup(dp0, dp1)
return dup
def sup(net: Net, sp0: Name, sp1: Name) -> Name:
sup = next(name)
net.vars[sup] = Sup(sp0, sp1)
return sup
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(sp0, sp1):
return f"+{{{show_pos(net, sp0)} {show_pos(net, sp1)}}}"
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(dp0, dp1):
return f"-{{{show_neg(net, dp0)} {show_neg(net, dp1)}}}"
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(sp0, sp1):
resolve_pos(net, sp0)
resolve_pos(net, sp1)
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(dp0, dp1):
resolve_neg(net, dp0)
resolve_neg(net, dp1)
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 Era(), Nil():
pass
case Era(), Lam(bnd, bod):
net.book.add((bnd, nil(net)))
net.book.add((era(net), bod))
case Era(), Sup(sp0, sp1):
net.book.add((era(net), sp0))
net.book.add((era(net), sp1))
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(sp0, sp1):
ap, an = wire(net)
bp, bn = wire(net)
cp, cn = wire(net)
dp, dn = wire(net)
net.book.add((dup(net, an, bn), arg))
net.book.add((ret, sup(net, cp, dp)))
net.book.add((app(net, ap, cn), sp0))
net.book.add((app(net, bp, dn), sp1))
case Dup(dp0, dp1), Nil():
net.book.add((dp0, nil(net)))
net.book.add((dp1, nil(net)))
case Dup(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, ap, cp)))
net.book.add((dup(net, bn, dn), bod))
case Dup(dp0, dp1), Sup(sp0, sp1):
net.book.add((dp0, sp0))
net.book.add((dp1, sp1))
return itrs
def print_state(net: Net, root: Name, *, wires: 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 wires:
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, *, wires: bool = False) -> None:
print("=" * 30)
print("=", "INITIAL".center(26), "=")
print("=" * 30)
print()
print_state(net, root, wires=wires)
print()
print("=" * 30)
print("=", "NORMALIZED".center(26), "=")
print("=" * 30)
print()
itrs = reduce(net)
resolve_pos(net, root)
print_state(net, root, wires=wires)
print()
print(f"ITRS: {itrs}")
def main() -> None:
net = empty_net()
root = nil(net)
print_reduction(net, root)
main()
Raw
polarized.py
import itertools
from collections.abc import Iterator
from dataclasses import dataclass
type Name = int
name = itertools.count()
type Pos = Var | Nil | Lam | Sup
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:
dp0: Neg
dp1: Neg
@dataclass(frozen=True)
class Sup:
sp0: Pos
sp1: Pos
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(sp0, sp1):
return f"+{{{show_pos(sp0)} {show_pos(sp1)}}}"
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(dp0, dp1):
return f"-{{{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(sp0, sp1):
return Sup(resolve_pos(sp0, vars, subs), resolve_pos(sp1, 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(dp0, dp1):
return Dup(resolve_neg(dp0, vars, subs), resolve_neg(dp1, vars, subs))
def rename_pos(pos: Pos, ctx: dict[Name, Name] | None = None, name: Iterator[Name] | None = None) -> Pos:
if ctx is None:
ctx = {}
if name is None:
name = itertools.count()
match pos:
case Var(nam) if nam in ctx:
return Var(ctx[nam])
case Var(nam):
ctx[nam] = next(name)
return Var(ctx[nam])
case Nil():
return Nil()
case Lam(bnd, bod):
return Lam(rename_neg(bnd, ctx, name), rename_pos(bod, ctx, name))
case Sup(sp0, sp1):
return Sup(rename_pos(sp0, ctx, name), rename_pos(sp1, ctx, name))
def rename_neg(neg: Neg, ctx: dict[Name, Name] | None = None, name: Iterator[Name] | None = None) -> Neg:
if ctx is None:
ctx = {}
if name is None:
name = itertools.count()
match neg:
case Sub(nam) if nam in ctx:
return Sub(ctx[nam])
case Sub(nam):
ctx[nam] = next(name)
return Sub(nam)
case Era():
return Era()
case App(arg, ret):
return App(rename_pos(arg, ctx, name), rename_neg(ret, ctx, name))
case Dup(dp0, dp1):
return Dup(rename_neg(dp0, ctx, name), rename_neg(dp1, ctx, name))
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(sp0, sp1):
book.add((Era(), sp0))
book.add((Era(), sp1))
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(sp0, sp1):
ap, an = wire()
bp, bn = wire()
cp, cn = wire()
dp, dn = wire()
book.add((Dup(an, bn), arg))
book.add((ret, Sup(cp, dp)))
book.add((App(ap, cn), sp0))
book.add((App(bp, dn), sp1))
case Dup(dp0, dp1), Nil():
book.add((dp0, Nil()))
book.add((dp1, Nil()))
case Dup(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(ap, cp)))
book.add((Dup(bn, dn), bod))
case Dup(dp0, dp1), Sup(sp0, sp1):
book.add((dp0, sp0))
book.add((dp1, sp1))
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)
renamed = rename_pos(resolved)
print_state(renamed, book)
print()
print(f"ITRS: {itrs}")
def main() -> None:
book = set[Rdx]()
root = Nil()
print_reduction(root, book)
main()
Raw
unpolarized.py
import itertools
from collections.abc import Iterator
from dataclasses import dataclass
type Name = int
name = itertools.count()
type Term = Var | Era | Con | Dup
@dataclass(frozen=True)
class Var:
nam: Name
@dataclass(frozen=True)
class Era:
pass
@dataclass(frozen=True)
class Con:
cn0: Term
cn1: Term
@dataclass(frozen=True)
class Dup:
dp0: Term
dp1: Term
def show(term: Term) -> str:
match term:
case Var(nam):
return f"{nam}"
case Era():
return "_"
case Con(cn0, cn1):
return f"({show(cn0)} {show(cn1)})"
case Dup(dp0, dp1):
return f"{{{show(dp0)} {show(dp1)}}}"
def resolve(term: Term, vars: dict[Name, Term]) -> Term:
match term:
case Var(nam) if nam in vars:
return resolve(vars[nam], vars)
case Var(nam):
return Var(nam)
case Era():
return Era()
case Con(cn0, cn1):
return Con(resolve(cn0, vars), resolve(cn1, vars))
case Dup(dp0, dp1):
return Dup(resolve(dp0, vars), resolve(dp1, vars))
def rename(term: Term, ctx: dict[Name, Name] | None = None, name: Iterator[Name] | None = None) -> Term:
if ctx is None:
ctx = {}
if name is None:
name = itertools.count()
match term:
case Var(nam) if nam in ctx:
return Var(ctx[nam])
case Var(nam):
ctx[nam] = next(name)
return Var(nam)
case Era():
return Era()
case Con(cn0, cn1):
return Con(rename(cn0, ctx, name), rename(cn1, ctx, name))
case Dup(dp0, dp1):
return Dup(rename(dp0, ctx, name), rename(dp1, ctx, name))
def var() -> Term:
return Var(next(name))
type Rdx = tuple[Term, Term]
def reduce(book: set[Rdx], vars: dict[Name, Term]) -> int:
itrs = 0
while book:
itrs += 1
match book.pop():
case ((Var(nam), other) | (other, Var(nam))) if nam in vars:
book.add((vars.pop(nam), other))
case (Var(nam), other) | (other, Var(nam)):
vars[nam] = other
case Era(), Era():
pass
case (Era(), Con(cn0, cn1)) | (Con(cn0, cn1), Era()):
book.add((Era(), cn0))
book.add((Era(), cn1))
case (Era(), Dup(dp0, dp1)) | (Dup(dp0, dp1), Era()):
book.add((Era(), dp0))
book.add((Era(), dp1))
case Con(cn00, cn01), Con(cn10, cn11):
book.add((cn00, cn10))
book.add((cn01, cn11))
case (Con(cn0, cn1), Dup(dp0, dp1)) | (Dup(dp0, dp1), Con(cn0, cn1)):
a = var()
b = var()
c = var()
d = var()
book.add((Dup(a, b), cn0))
book.add((Dup(c, d), cn1))
book.add((Con(a, c), dp0))
book.add((Con(b, d), dp1))
case Dup(dp00, dp01), Dup(dp10, dp11):
book.add((dp00, dp10))
book.add((dp01, dp11))
return itrs
def print_state(root: Term, book: set[Rdx]) -> None:
print("ROOT:")
print(f" {show(root)}")
print()
print("BOOK:")
for lhs, rhs in book:
print(f" {show(lhs)} ⋈ {show(rhs)}")
def print_reduction(root: Term, book: set[Rdx]) -> None:
vars: dict[Name, Term] = {}
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)
resolved = resolve(root, vars)
renamed = rename(resolved)
print_state(renamed, book)
print()
print(f"ITRS: {itrs}")
def main() -> None:
book = set[Rdx]()
root = Era()
print_reduction(root, book)
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment