/src/main.py at b24bc6eec345580b1447c1ecbbd01c2782a00a94

# Don't use any features above Python 3.9!
# Since that's what Ren'Py uses
# So no pattern matching sadly
# Format with ruff format lambcalc.py
# Must specify file or it'll mess with the vendored deps too

import sys
from random import randrange
from typing import Any, NamedTuple


## Lambda term
class L(NamedTuple):
    var: int
    body: Any


# Application term
class A(NamedTuple):
    fn: Any
    arg: Any


# Recursively substitute var with rep in term
def sub(term, var, rep):
    if type(term) is L:
        # assert term.var != var
        if term.var == var:
            # Shadowing
            return term
        return L(term.var, sub(term.body, var, rep))
    if type(term) is A:
        return A(sub(term.fn, var, rep), sub(term.arg, var, rep))
    if term == var:
        return rep
    return term


# Add offset to all bound vars
def alpha(term, offset, bound):
    if type(term) is L:
        return L(term.var + offset, alpha(term.body, offset, bound | {term.var}))
    if type(term) is A:
        return A(alpha(term.fn, offset, bound), alpha(term.arg, offset, bound))
    # if term in bound:
        return term + offset
    return term


# Simplify term using beta reduction
def red(term):
    if type(term) is L:
        return L(term.var, red(term.body))
    if type(term) is A:
        fn = red(term.fn)
        if type(fn) is L:
            # Rename bound vars in fn.body to avoid name collisions
            return red(sub(fn.body, fn.var, alpha(term.arg, randrange(10**8), set())))
        return A(fn, red(term.arg))
    return term


# Simplify term using beta reduction without var renaming
def red_dumb(term):
    if type(term) is L:
        return L(term.var, red_dumb(term.body))
    if type(term) is A:
        fn = red_dumb(term.fn)
        if type(fn) is L:
            return red_dumb(sub(fn.body, fn.var, term.arg))
        return A(fn, red_dumb(term.arg))
    return term


# Rename vars using first available int
# Input term must be reduced first
def canonicalize(term, bound, free):
    if type(term) is L:
        # Shadowing should never happen
        assert not term.var in bound
        if len(bound) == 0 and len(free) == 0:
            var2 = 1
        else:
            var2 = max((bound | free).values()) + 1
        return L(var2, canonicalize(term.body, bound | {term.var: var2}, free))
    if type(term) is A:
        return A(
            canonicalize(term.fn, bound, free), canonicalize(term.arg, bound, free)
        )
    if term in bound:
        return bound[term]
    if len(bound) == 0 and len(free) == 0:
        free[term] = 1
    elif not term in free:
        free[term] = max((bound | free).values()) + 1
    return free[term]


# Get size of term
def size(term):
    if type(term) is L:
        return 1 + size(term.body)
    if type(term) is A:
        return size(term.fn) + size(term.arg)
    return 1


# Check equality
def eq(term1, term2):
    return canonicalize(term1, {}, {}) == canonicalize(term2, {}, {})


animals = " 🦊🐱🐸🐷🐼🐶🐭🐻🐨🐯🐺🦁🐮🐹🐰🐵🦝🤔😱"


# Get friendly uncurried repr of canon term
def animal_repr_canon(term):
    if type(term) is str:
        return term
    if type(term) is L:
        if type(term.body) is L:
            return f"{animal_repr_canon(term.var)}{animal_repr_canon(term.body)}"
        return f"{animal_repr_canon(term.var)}->{animal_repr_canon(term.body)}|"
    if type(term) is A:
        return f"{animal_repr_canon(term.fn)}({animal_repr_canon(term.arg)})"
    return animals[term]


# Wrapper func
def animal_repr(term):
    return animal_repr_canon(canonicalize(term, {}, {}))


# https://en.wikipedia.org/wiki/SKI_combinator_calculus
I = L(1, 1)
K = L(1, L(2, 1))
S = L(1, L(2, L(3, A(A(1, 3), A(2, 3)))))
# https://en.wikipedia.org/wiki/Fixed-point_combinator
# red(Y) doesn't terminate though...
Y = L(1, A(L(2, A(1, A(2, 2))), L(2, A(1, A(2, 2)))))
Z = L(1, A(L(2, A(1, L(3, A(A(2, 2), 3)))), L(2, A(1, L(3, A(A(2, 2), 3))))))

# From https://lambster.dev/
# Same as K
ltrue = L(1, L(2, 1))
lfalse = L(1, L(2, 2))
land = L(1, L(2, A(A(1, 2), 1)))
lor = L(1, L(2, A(A(1, 1), 2)))
lnot = L(1, A(A(1, lfalse), ltrue))
lif = L(1, L(2, L(3, A(A(1, 2), 3))))
# Can also use pair/first/second for lists
lpair = L(1, L(2, L(3, A(A(3, 1), 2))))
lfirst = L(1, A(1, ltrue))
lsecond = L(1, A(1, lfalse))
lnil = L(1, ltrue)
lnull = L(1, A(1, L(2, L(3, lfalse))))
ltree = L(1, L(2, L(3, A(A(1, 2), 3))))
ldatum = L(1, A(1, lfirst))
lleft = L(1, A(A(1, lsecond), lfirst))
lright = L(1, A(1, lsecond))
lincr = L(1, L(2, L(3, A(2, A(A(1, 2), 3)))))
lplus = L(1, L(2, A(1, lincr)))
ltimes = L(1, L(2, A(1, A(lplus, 2))))
liszero = L(1, A(A(1, L(2, lfalse)), ltrue))
# Church numerals
lzero = lfalse
lone = L(1, L(2, A(1, 2)))
ltwo = L(1, L(2, A(1, A(1, 2))))
lthree = L(1, L(2, A(1, A(1, A(1, 2)))))
lfour = L(1, L(2, A(1, A(1, A(1, A(1, 2))))))
lfive = L(1, L(2, A(1, A(1, A(1, A(1, A(1, 2)))))))
lsix = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, 2))))))))
lseven = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, A(1, 2)))))))))
leight = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, A(1, A(1, 2))))))))))
lnine = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, A(1, A(1, A(1, 2)))))))))))


# Tests
assert eq(red(A(A(A(S, K), I), A(A(K, I), S))), I)
assert eq(red(A(A(A(S, K), S), K)), K)
assert eq(red(A(A(A(S, K), I), K)), K)
assert eq(red(A(A(K, S), A(I, A(A(A(S, K), S), I)))), S)
# eta reduction
assert eq(red(L(1, A(L(2, A(2, 2)), 1))), L(1, A(1, 1)))
# Rename bound variable in lambda after name collision
assert eq(red(A(K, K)), L(1, L(2, L(3, 2))))
# Avoid name capture of bound variables
# https://www.cs.yale.edu/homes/hudak/CS201S08/lambda.pdf
assert eq(red(A(L(1, L(2, 1)), 2)), L(2, 3))
# Should two free vars refer to the same var??
# Like maybe we should just assume all vars are bound above us somewhere
# I think that massively simplifies the code, since then red doesn't need to track currently bound vars
# I should choose the one that makes for better puzzles
assert eq(red(A(L(1, A(2, 1)), 2)), A(2, 2))


# Brute force!!
def solve(terms, moves, depth):
    cnt = sum(type(term) is int for term in terms)
    if cnt == len(terms):
        print(moves)
        return
    if len(terms) - cnt > depth:
        # Can only increase cnt by one per turn anyways
        return
    for i in range(len(terms)):
        for j in range(len(terms)):
            newterms = terms.copy()
            try:
                newterms[j] = red_dumb(A(terms[i], terms[j]))
                # if size(newterms[j]) > 50:
                # Heuristic: stop if term is blowing up
                # continue
            except:
                continue
            solve(newterms, moves + [i, j], depth - 1)


if __name__ == "__main__":
    sys.setrecursionlimit(50)
    # solve([A(1, 3), L(5, L(2, 5)), L(1, L(2, 2))], [], 9)