k-SIC + universal δ (UDP/USP)

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

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


@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


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)}}}"


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 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 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 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))
    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_zero() -> Pos:
    # λf.λx.x
    xp, xn = wire()
    return Lam(Era(), Lam(xn, xp))


def mk_succ(book: set[Rdx]) -> Pos:
    # λn.λf.λx.(f ((n f) x))
    np, nn = wire()
    f0p, f0n = wire()
    f1p, f1n = wire()
    xp, xn = wire()
    return Lam(nn, Lam(Udp(f0n, f1n), Lam(xn, mk_app(book, f1p, mk_app(book, mk_app(book, np, f0p), xp)))))


def mk_one(book: set[Rdx], zero: Pos, succ: Pos) -> Pos:
    # (succ zero)
    return mk_app(book, succ, zero)


def mk_two(book: set[Rdx], one: Pos, succ: Pos) -> Pos:
    # (succ one)
    return mk_app(book, succ, one)


def mk_three(book: set[Rdx], two: Pos, succ: Pos) -> Pos:
    # (succ two)
    return mk_app(book, succ, two)


def mk_add(book: set[Rdx], succ: Pos) -> Pos:
    # λa.λb.((b succ) a)
    ap, an = wire()
    bp, bn = wire()
    return Lam(an, Lam(bn, mk_app(book, mk_app(book, bp, succ), ap)))


def mk_mul(book: set[Rdx], zero: Pos, add: Pos) -> Pos:
    # λa.λb.((b (add a)) zero)
    ap, an = wire()
    bp, bn = wire()
    return Lam(an, Lam(bn, mk_app(book, mk_app(book, bp, mk_app(book, add, ap)), zero)))


def mk_exp(book: set[Rdx], one: Pos, mul: Pos) -> Pos:
    # λa.λb.((b (mul a)) one)
    ap, an = wire()
    bp, bn = wire()
    return Lam(an, Lam(bn, mk_app(book, mk_app(book, bp, mk_app(book, mul, ap)), one)))


def mk_tet(book: set[Rdx], one: Pos, exp: Pos) -> Pos:
    # λa.λb.((b (exp a)) one)
    ap, an = wire()
    bp, bn = wire()
    return Lam(an, Lam(bn, mk_app(book, mk_app(book, bp, mk_app(book, exp, ap)), one)))


def mk_test_sharing(book: set[Rdx], zero: Pos, succ: Pos) -> Pos:
    """
    Test UDP & USP by translating a logarithmic encoding of 16 into linear.
    """

    # λf.λx.(f (f x))
    f0p, f0n = wire()
    f1p, f1n = wire()
    xp, xn = wire()
    two = Lam(Udp(f0n, f1n), Lam(xn, mk_app(book, f1p, mk_app(book, f0p, xp))))

    # (two two two)
    two0, two = mk_udp(book, two)
    two1, two = mk_udp(book, two)
    two2, two = mk_udp(book, two)
    n = mk_app(book, mk_app(book, two0, two1), two2)
    # return n

    # ((n succ) zero)
    return mk_app(book, mk_app(book, n, succ), zero)


def mk_root(book: set[Rdx], two: Pos, three: Pos, tet: Pos) -> Pos:
    # ((tet two) three)
    return mk_app(book, mk_app(book, tet, two), three)


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

    zero = mk_zero()

    succ = mk_succ(book)

    zero0, zero = mk_udp(book, zero)
    succ0, succ = mk_udp(book, succ)
    one = mk_one(book, zero0, succ0)

    one0, one = mk_udp(book, one)
    succ0, succ = mk_udp(book, succ)
    two = mk_two(book, one0, succ0)

    two0, two = mk_udp(book, two)
    succ0, succ = mk_udp(book, succ)
    three = mk_three(book, two0, succ0)

    succ0, succ = mk_udp(book, succ)
    add = mk_add(book, succ0)

    zero0, zero = mk_udp(book, zero)
    add0, add = mk_udp(book, add)
    mul = mk_mul(book, zero0, add0)

    one0, one = mk_udp(book, one)
    mul0, mul = mk_udp(book, mul)
    exp = mk_exp(book, one0, mul0)

    one0, one = mk_udp(book, one)
    exp0, exp = mk_udp(book, exp)
    tet = mk_tet(book, one0, exp0)

    two0, two = mk_udp(book, two)
    three0, three = mk_udp(book, three)
    tet0, tet = mk_udp(book, tet)
    root = mk_root(book, two0, three0, tet0)

    print_reduction(root, book)


main()