/lambcalc.py at a51dc51da2eae7e717a127856c81b98246f2fe30

# Don't use any features above Python 3.9!
# Since that's what Ren'Py uses
# So no pattern matching sadly

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:
        # Shadowing should never happen
        assert term.var != var
        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(alpha(fn.body, randrange(10**8), set()), fn.var, term.arg))
        return A(fn, red(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 = 0
        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] = 0
    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 L:
        if type(term.body) is L:
            return f"{animals[term.var]}{animal_repr_canon(term.body)}"
        return f"{animals[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))))))

# 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(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)

# Tech
# L(1, 2): make this and you instawin
# L(1, 1): identity
# K = L(1, L(2, 1)), L(1, L(2, L(3, 2))) autored toggle

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

    # solve([L(1, L(2, L(3, 1))), A(1, A(2, L(3, 4)))], [], 10)
    # solve([L(1, L(2, 1)), L(1, A(A(A(A(1, 2), 3), 4), L(5, 6))), L(1, A(1, 1))], [], 8)

    # solve([L(1, L(2, 1)), L(1, L(2, 1)), A(A(1, 2), L(1, 1))], [], 9)

    solve([])