k-SIC + unordered δ + refcount

sic.py

import itertools

from dataclasses import dataclass


type Name = int

name = itertools.count()


type Label = int

label = itertools.count()


type Pos = Var | Lam | Sup | Usp | Rep

type Neg = Sub | App | Dup | Udp | Acc


@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:
    udl: Label
    ud0: Name
    ud1: Name


@dataclass(frozen=True)
class Usp:
    usl: Label
    us0: Name
    us1: Name


@dataclass(frozen=True)
class Rep:
    rpl: Label
    rpb: Name


@dataclass(frozen=True)
class Acc:
    acl: Label
    acb: 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, udl: Label, ud0: Name, ud1: Name) -> Name:
    udp = next(name)
    net.subs[udp] = Udp(udl, ud0, ud1)
    return udp


def usp(net: Net, usl: Label, us0: Name, us1: Name) -> Name:
    usp = next(name)
    net.vars[usp] = Usp(usl, us0, us1)
    return usp


def rep(net: Net, rpl: Label, rpb: Name) -> Name:
    rep = next(name)
    net.vars[rep] = Rep(rpl, rpb)
    return rep


def acc(net: Net, acl: Label, acb: Name) -> Name:
    acc = next(name)
    net.subs[acc] = Acc(acl, acb)
    return acc


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 Usp(usl, us0, us1):
            return f"+%{usl}[{show_pos(net, us0)} {show_pos(net, us1)}]"
        case Rep(rpl, rpb):
            return f"+%{rpl}{{{show_pos(net, rpb)}}}"


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 Udp(udl, ud0, ud1):
            return f"-%{udl}[{show_neg(net, ud0)} {show_neg(net, ud1)}]"
        case Acc(acl, acb):
            return f"-%{acl}{{{show_neg(net, acb)}}}"


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 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(usl, us0, us1):
                ap, an = wire(net)
                bp, bn = wire(net)
                cp, cn = wire(net)
                dp, dn = wire(net)
                net.book.add((dup(net, usl, an, bn), arg))
                net.book.add((ret, sup(net, usl, cp, dp)))
                net.book.add((app(net, ap, cn), us0))
                net.book.add((app(net, bp, dn), us1))
            case App(arg, ret), Rep(rpl, rpb):
                x = next(name)
                net.vars[x] = net.vars.pop(rpb)
                ap, an = wire(net)
                net.book.add((udp(net, rpl, app(net, arg, ret), an), x))
                net.vars[rpb] = net.vars.pop(ap)

            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(usl, us0, us1) if dpl == usl:
                net.book.add((dp0, us0))
                net.book.add((dp1, us1))
            case Dup(dpl, dp0, dp1), Usp(usl, us0, us1):
                net.book.add((dup(net, dpl, acc(net, usl, dp0), acc(net, usl, dp1)), us0))
                net.book.add((dup(net, dpl, acc(net, usl, dp0), acc(net, usl, dp1)), us1))
            case Dup(dpl, dp0, dp1), Rep(rpl, rpb) if dpl == rpl:
                net.book.add((dp0, rep(net, rpl, rpb)))
                net.book.add((dp1, rep(net, rpl, rpb)))
            case Dup(dpl, dp0, dp1), Rep(rpl, rpb):
                x = next(name)
                net.vars[x] = net.vars.pop(rpb)
                ap, an = wire(net)
                net.book.add((udp(net, rpl, dup(net, dpl, dp0, dp1), an), x))
                net.vars[rpb] = net.vars.pop(ap)

            case Udp(udl, ud0, ud1), Lam(bnd, bod):
                ap, an = wire(net)
                bp, bn = wire(net)
                cp, cn = wire(net)
                dp, dn = wire(net)
                net.book.add((bnd, sup(net, udl, ap, bp)))
                net.book.add((dup(net, udl, cn, dn), bod))
                net.book.add((ud0, lam(net, an, cp)))
                net.book.add((ud1, lam(net, bn, dp)))
            case Udp(udl, ud0, ud1), Sup(spl, sp0, sp1) if udl == spl:
                net.book.add((ud0, sp0))
                net.book.add((ud1, sp1))
            case Udp(udl, ud0, ud1), Sup(spl, sp0, sp1):
                net.book.add((ud0, sup(net, spl, rep(net, udl, sp0), rep(net, udl, sp1))))
                net.book.add((ud1, sup(net, spl, rep(net, udl, sp0), rep(net, udl, sp1))))
            case Udp(udl, ud0, ud1), Usp(usl, us0, us1) if udl == usl:
                net.book.add((ud0, us0))
                net.book.add((ud1, us1))
            case Udp(udl, ud0, ud1), Usp(usl, us0, us1):
                ap, an = wire(net)
                bp, bn = wire(net)
                cp, cn = wire(net)
                dp, dn = wire(net)
                net.book.add((ud0, usp(net, usl, ap, bp)))
                net.book.add((ud1, usp(net, usl, cp, dp)))
                net.book.add((udp(net, udl, an, cn), us0))
                net.book.add((udp(net, udl, bn, dn), us1))
            case Udp(udl, ud0, ud1), Rep(rpl, rpb) if udl == rpl:
                net.book.add((ud0, rep(net, rpl, rpb)))
                net.book.add((ud1, rep(net, rpl, rpb)))
            case Udp(udl, ud0, ud1), Rep(rpl, rpb):
                x = next(name)
                net.vars[x] = net.vars.pop(rpb)
                ap, an = wire(net)
                net.book.add((udp(net, rpl, udp(net, udl, ud0, ud1), an), x))
                net.vars[rpb] = net.vars.pop(ap)

            case Acc(acl, acb), Lam(bnd, bod):
                x = next(name)
                net.subs[x] = net.subs.pop(acb)
                ap, an = wire(net)
                net.book.add((x, usp(net, acl, lam(net, bnd, bod), ap)))
                net.subs[acb] = net.subs.pop(an)
            case Acc(acl, acb), Sup(spl, sp0, sp1) if acl == spl:
                net.book.add((acc(net, acl, acb), sp0))
                net.book.add((acc(net, acl, acb), sp1))
            case Acc(acl, acb), Sup(spl, sp0, sp1):
                x = next(name)
                net.subs[x] = net.subs.pop(acb)
                ap, an = wire(net)
                net.book.add((x, usp(net, acl, sup(net, spl, sp0, sp1), ap)))
                net.subs[acb] = net.subs.pop(an)
            case Acc(acl, acb), Usp(usl, us0, us1) if acl == usl:
                net.book.add((acc(net, acl, acb), us0))
                net.book.add((acc(net, acl, acb), us1))
            case Acc(acl, acb), Usp(usl, us0, us1):
                x = next(name)
                net.subs[x] = net.subs.pop(acb)
                ap, an = wire(net)
                net.book.add((x, usp(net, acl, usp(net, usl, us0, us1), ap)))
                net.subs[acb] = net.subs.pop(an)
            # case Acc(acl, acb), Rep(rpl, rpb) if acl == rpl:
            #     ...
            case Acc(acl, acb), Rep(rpl, rpb):
                x = next(name)
                net.subs[x] = net.subs.pop(acb)
                ap, an = wire(net)
                net.book.add((x, usp(net, acl, rep(net, rpl, rpb), ap)))
                net.subs[acb] = net.subs.pop(an)

    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_rep(net: Net, x: Name, n: int, lab: Label | None = None) -> list[Name]:
    if lab is None:
        lab = next(label)
    return [rep(net, lab, x) for _ in range(n)]


def mk_c2(net: Net) -> Name:
    fp, fn = wire(net)
    xp, xn = wire(net)
    
    f0, f1 = mk_dup(net, fp)

    fx  = mk_app(net, f0, xp)
    ffx = mk_app(net, f1, fx)

    return lam(net, fn, 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_rep(net, fp, 2)
    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_rep(net, lam(net, yn, yp), 2)
    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()