SIC + new agent fusion showcase

sic.py

import itertools

from dataclasses import dataclass


type Name = int

name = itertools.count()


type Label = int

label = itertools.count()


type Term = Pos | Neg

type Pos = Var | Nil | Lam | Sup | Usp | Lsp

type Neg = Sub | Era | App | Dup | Udp | Ldp


@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 Udp:
    ud0: Neg
    ud1: Neg


@dataclass(frozen=True)
class Usp:
    us0: Pos
    us1: Pos


@dataclass(frozen=True)
class Ldp:
    ldl: Label
    ld0: Neg
    ld1: Neg


@dataclass(frozen=True)
class Lsp:
    lsl: Label
    ls0: Pos
    ls1: Pos


def show(term: Term, vars: dict[Name, Pos] = {}, subs: dict[Name, Neg] = {}) -> str:
    match term:
        case Var(nam) if nam in vars:
            return show(vars[nam], vars, subs)
        case Var(nam):
            return f"+{nam}"
        case Sub(nam) if nam in subs:
            return show(subs[nam], vars, subs)
        case Sub(nam):
            return f"-{nam}"
        case Nil():
            return "+_"
        case Era():
            return "-_"
        case Lam(bnd, bod):
            return f"+({show(bnd, vars, subs)} {show(bod, vars, subs)})"
        case App(arg, ret):
            return f"-({show(arg, vars, subs)} {show(ret, vars, subs)})"
        case Dup(dpl, dp0, dp1):
            return f"-&{dpl}{{{show(dp0, vars, subs)} {show(dp1, vars, subs)}}}"
        case Sup(spl, sp0, sp1):
            return f"+&{spl}{{{show(sp0, vars, subs)} {show(sp1, vars, subs)}}}"
        case Udp(ud0, ud1):
            return f"-{{{show(ud0, vars, subs)} {show(ud1, vars, subs)}}}"
        case Usp(us0, us1):
            return f"+{{{show(us0, vars, subs)} {show(us1, vars, subs)}}}"
        case Ldp(ldl, ld0, ld1):
            return f"-&{ldl}[{show(ld0, vars, subs)} {show(ld1, vars, subs)}]"
        case Lsp(lsl, ls0, ls1):
            return f"+&{lsl}[{show(ls0, vars, subs)} {show(ls1, 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(), Usp(us0, us1):
                book.add((Era(), us0))
                book.add((Era(), us1))
            case Era(), Lsp(lsl, ls0, ls1):
                # Probably same as ERA~SUP
                raise RuntimeError("ERA~LSP Undiscovered")

            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), Usp(us0, us1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                lab = next(label)
                book.add((Dup(lab, an, bn), arg))
                book.add((ret, Sup(lab, cp, dp)))
                book.add((App(ap, cn), us0))
                book.add((App(bp, dn), us1))
            case App(arg, ret), Lsp(lsl, ls0, ls1):
                # Probably same as APP~SUP
                raise RuntimeError("APP~LSP Undiscovered")

            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), Usp(us0, us1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((dp0, Usp(ap, bp)))
                book.add((dp1, Usp(cp, dp)))
                book.add((Dup(dpl, an, cn), us0))
                book.add((Dup(dpl, bn, dn), us1))
            case Dup(dpl, dp0, dp1), Lsp(lsl, ls0, ls1) if dpl == lsl:
                book.add((dp0, ls0))
                book.add((dp1, ls1))
            case Dup(dpl, dp0, dp1), Lsp(lsl, ls0, ls1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((dp0, Lsp(lsl, ap, bp)))
                book.add((dp1, Lsp(lsl, cp, dp)))
                book.add((Dup(dpl, an, cn), ls0))
                book.add((Dup(dpl, bn, dn), ls1))

            case Udp(ud0, ud1), Nil():
                book.add((ud0, Nil()))
                book.add((ud1, Nil()))
            case Udp(ud0, ud1), Lam(bnd, bod):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                lab = next(label)
                book.add((ud0, Lam(an, bp)))
                book.add((ud1, Lam(cn, dp)))
                book.add((bnd, Sup(lab, ap, cp)))
                book.add((Dup(lab, bn, dn), bod))
            case Udp(ud0, ud1), Sup(spl, sp0, sp1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((ud0, Sup(spl, ap, bp)))
                book.add((ud1, Sup(spl, cp, dp)))
                book.add((Udp(an, cn), sp0))
                book.add((Udp(bn, dn), sp1))
            case Udp(ud0, ud1), Usp(us0, us1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((ud0, Usp(ap, bp)))
                book.add((ud1, Usp(cp, dp)))
                book.add((Udp(an, cn), us0))
                book.add((Udp(bn, dn), us1))
            case Udp(ud0, ud1), Lsp(lsl, ls0, ls1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((ud0, Lsp(lsl, ap, bp)))
                book.add((ud1, Lsp(lsl, cp, dp)))
                book.add((Udp(an, cn), ls0))
                book.add((Udp(bn, dn), ls1))

            case Ldp(ldl, ld0, ld1), Nil():
                # Probably same as DUP~NIL
                raise RuntimeError("LDP~NIL Undiscovered")
            case Ldp(ldl, ld0, ld1), Lam(bnd, bod):
                # Probably same as DUP~LAM
                raise RuntimeError("LDP~LAM Undiscovered")
            case Ldp(ldl, ld0, ld1), Sup(spl, sp0, sp1) if ldl == spl:
                book.add((ld0, sp0))
                book.add((ld1, sp1))
            case Ldp(ldl, ld0, ld1), Sup(spl, sp0, sp1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((ld0, Sup(spl, ap, bp)))
                book.add((ld1, Sup(spl, cp, dp)))
                book.add((Ldp(ldl, an, cn), sp0))
                book.add((Ldp(ldl, bn, dn), sp1))
            case Ldp(ldl, ld0, ld1), Usp(us0, us1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((ld0, Usp(ap, bp)))
                book.add((ld1, Usp(cp, dp)))
                book.add((Ldp(ldl, an, cn), us0))
                book.add((Ldp(ldl, bn, dn), us1))
            case Ldp(ldl, ld0, ld1), Lsp(lsl, ls0, ls1) if ldl == lsl:
                book.add((ld0, Sup(ldl, ls0, ls1)))
                book.add((ld1, Nil()))
            case Ldp(ldl, ld0, ld1), Lsp(lsl, ls0, ls1):
                # Probably same as DUP~SUP
                raise RuntimeError("LDP~LSP Undiscovered")
    return itrs


def print_state(root: Term, book: set[Rdx], vars: dict[Name, Pos], subs: dict[Name, Neg]) -> None:
    print("ROOT:")
    print(f"  {show(root, vars, subs)}")
    print()
    print("BOOK:")
    for lhs, rhs in book:
        print(f"  {show(lhs, vars, subs)} ⋈ {show(rhs, vars, subs)}")


def print_reduction(root: Term, 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, vars, subs)
    print()

    print("=" * 30)
    print("=", "REDUCED".center(26), "=")
    print("=" * 30)
    print()

    itrs = reduce(book, vars, subs)

    print_state(root, book, vars, subs)
    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_udp(book: set[Rdx], x: Pos) -> tuple[Pos, Pos]:
    x0p, x0n = wire()
    x1p, x1n = wire()
    book.add((Udp(x0n, x1n), x))
    return x0p, x1p


def mk_c2(book: set[Rdx]) -> Pos:
    f0p, f0n = wire()
    f1p, f1n = wire()
    xp, xn = wire()

    fx  = mk_app(book, f1p, xp)
    ffx = mk_app(book, f0p, fx)

    return Lam(Udp(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)


# \ft. L{f,t}=ft; t
def mk_true(bool_lab: Label) -> Pos:
    tp, tn = wire()
    return Lam(Dup(bool_lab, Era(), tn), tp)


# \b.\ft. L[f,t]=ft; L{f0,f1}=f; (b L[f0,f1])
def mk_clr(bool_lab: Label) -> Pos:
    f0p, f0n = wire()
    f1p, f1n = wire()
    rp, rn = wire()
    return Lam(App(Lsp(bool_lab, f0p, f1p), rn), Lam(Ldp(bool_lab, Dup(bool_lab, f0n, f1n), Era()), rp))


def main() -> None:
    book = set[Rdx]()

    bool_lab = next(label)
    true = mk_true(bool_lab)
    clr = mk_clr(bool_lab)

    N = 100
    c_2powN = mk_cpow2(book, N)
    clr_2powN = mk_app(book, c_2powN, clr)
    root = mk_app(book, clr_2powN, true)

    print_reduction(root, book)


main()