t.py

from collections.abc import Callable
from dataclasses import dataclass


def curry[First, *Rest, Result](
    function: Callable[[First, *Rest], Result],
) -> Callable[[*Rest], Callable[[First], Result]]:
    return lambda *rest: lambda first: function(first, *rest)


type Term = Index | Abstraction | Application


@dataclass(frozen=True)
class Index:
    value: int


@dataclass(frozen=True)
class Abstraction:
    body: Term


@dataclass(frozen=True)
class Application:
    body: Term
    argument: Term


def term_reduce(term: Term) -> Term:
    match term:
        case Application(Abstraction(body), argument):
            return term_replace(argument)(0)(body)
        case Application(body, argument):
            return Application(term_reduce(body), argument)
        case _:
            return term


@curry
@curry
def term_replace(where: Term, depth: int, to_what: Term) -> Term:
    match where:
        case Index(index):
            return to_what if index == depth else where
        case Abstraction(body):
            return Abstraction(term_replace(to_what)(depth + 1)(body))
        case Application(body, argument):
            return Application(
                term_replace(to_what)(depth)(body),
                term_replace(to_what)(depth)(argument),
            )


def term_show(term: Term) -> str:
    match term:
        case Index(index):
            return f"{index}"
        case Abstraction(body):
            return f"λ {term_show(body)}"
        case Application(body, argument):
            return f"({term_show(body)}) ({term_show(argument)})"


@curry
def term_equal(first: Term, second: Term) -> bool:
    match first, second:
        case Index(first_index), Index(second_index):
            return first_index == second_index
        case Abstraction(first_abstraction), Abstraction(second_abstraction):
            return term_equal(second_abstraction)(first_abstraction)
        case Application(
            first_application_body, first_application_argument
        ), Application(second_application_body, second_application_argument):
            return term_equal(second_application_body)(
                first_application_body
            ) and term_equal(second_application_argument)(first_application_argument)
        case _:
            return False


def main() -> None:
    program = Application(
        Abstraction(
            Abstraction(
                Application(
                    Index(1),
                    Index(0),
                ),
            ),
        ),
        Abstraction(
            Application(
                Index(0),
                Index(0),
            ),
        ),
    )

    print(term_show(program))

    while not term_equal(program)(program := term_reduce(program)):
        print(term_show(program))


main()