diff --git a/checker/lib/basic.py b/checker/lib/basic.py index a0561e2..4b2a9ac 100644 --- a/checker/lib/basic.py +++ b/checker/lib/basic.py @@ -4,30 +4,32 @@ # from ..proof import Context, Proof from ..props import Eq, Or, Prop -from ..terms import App, Const, EqT, Lambda, Term, Var, register_known_const +from ..terms import App, Const, A1, A2, L1, L2, L3, Lambda, Term, Var, register_known_const # ----------------------------------------------------------------------------- # Identity function # ----------------------------------------------------------------------------- # Always returns its input. -register_known_const("identity", Lambda(Var(0))) +id_func = Lambda(lambda x : x) +register_known_const("id", id_func) +register_known_const("identity", id_func) -# ----------------------------------------------------------------------------- -# Equality -# ----------------------------------------------------------------------------- -equality = Lambda(Lambda(EqT(lhs=Var(1), rhs=Var(0)))) +# # ----------------------------------------------------------------------------- +# # Equality +# # ----------------------------------------------------------------------------- +# equality = Lambda(Lambda(EqT(lhs=Var(1), rhs=Var(0)))) -register_known_const("eq", equality) -register_known_const("==", equality) +# register_known_const("eq", equality) +# register_known_const("==", equality) # ----------------------------------------------------------------------------- # Bool # ----------------------------------------------------------------------------- -bool_t = Lambda(Lambda(Var(1))) -bool_f = Lambda(Lambda(Var(0))) -if_statement = Lambda(Var(0)) -not_statement = Lambda(App(f=App(f=Var(0), x=bool_f), x=bool_t)) +bool_t = L2(lambda x, y : x).normalize() +bool_f = L2(lambda x, y : y).normalize() +if_statement = L3(lambda x, y, z : A2(x, y, z)).normalize() +not_statement = L1(lambda b : A2(b, bool_f, bool_t)).normalize() register_known_const("Bool.False", bool_f) register_known_const("Bool.True", bool_t) @@ -50,25 +52,15 @@ def kernel_from_int(n : int) -> Term: raise ValueError( "Int is not Nat" ) - elif n == 0: - return zero - else: - return App(f=succ, x=kernel_from_int(n-1)) -def is_nat(x : Term) -> Prop: - return Or( - Eq(x=x, y=zero), - Eq(bool_f, bool_t) # TODO: Construct x = Succ n where isNat(n), - ) + t = zero + for _ in range(n): + t = A1(succ, t) -register_known_const("Nat.add", Lambda(Lambda( - App(f=App( # If-statement: is the first argument zero? - f=EqT(lhs=Var(1), rhs=zero), - # If so, return the second argument - x=Var(0), - ), - # If not, return a recursive solution of the add function - # TODO: Not correct yet - x=App(f=succ, x=App(f=App(f=Const("Nat.add"), x=Var(1)), x=Var(0))) - ) -))) + return t + +# def is_nat(x : Term) -> Prop: +# return Or( +# Eq(x=x, y=zero), +# Eq(bool_f, bool_t) # TODO: Construct x = Succ n where isNat(n), +# ) diff --git a/checker/proof.py b/checker/proof.py index d218981..251c805 100644 --- a/checker/proof.py +++ b/checker/proof.py @@ -238,9 +238,10 @@ def reflexivity(eq : Eq) -> Proof: statement=eq, ) else: - diff_l, diff_r = l.reduce_on_equality(r) + # diff_l, diff_r = l.reduce_on_equality(r) raise ProofCheckerFailedException( - f"Could not normalize {eq.x} = {eq.y}, got stuck at {diff_l} = {diff_r}" + f"Could not normalize {eq.x} = {eq.y}, got stuck at {l} = {r}" + # f"Could not normalize {eq.x} = {eq.y}, got stuck at {diff_l} = {diff_r}" ) def suppose(ctx : Context, proof : Proof) -> Proof: diff --git a/checker/terms.py b/checker/terms.py index 3890b3d..09642ee 100644 --- a/checker/terms.py +++ b/checker/terms.py @@ -4,43 +4,170 @@ """ from __future__ import annotations +from typing import Callable import copy from dataclasses import dataclass +# Known const values that can be substituted into other values. _known_consts : dict[str, Term] = {} +# Known functions to normalize certain specific terms with given shapes. +_known_norms : list[Callable[[Term], Term]] = [] + +USABLE_VAR_NAMES = [ + 'x', 'y', 'z', 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', + 'm', 'n', 'o', 'p', 'q', 'r', 's', 't', 'u', 'v', 'w', + 'α', 'β', 'γ', 'δ', 'ε', 'ζ', 'η', 'θ', 'ι', 'κ', + # 'λ', # Avoid confusion + 'μ', 'ν', 'ξ', 'ο', 'π', 'ρ', 'σ', 'τ', 'υ', 'φ', 'χ', 'ψ', 'ω' +] + +def normalize(term : Term) -> Term: + """ + Create a normalization function. This function simplifies functions as + much as possible. + """ + + def norm_iter(term : Term) -> Term: + """ + Normalize a single term. Trust that all children values have + already been normalized, or that they will be normalized later on. + + :param term: The term to normalize. + :type term: Term + :return: A normalized version of the term. + :rtype: Term + """ + match term: + case App(): + match term.f: + case Lambda(): + return term.f.substitute(value=norm_iter(term.x)) + + case _: + return term + + case Const(): + return _known_consts.get(term.name, term) + + case Lambda(): + return term + + case Var(): + return term + + case Term(): + return term + + return traverse(f=norm_iter, term=term) + def register_known_const(name : str, value : Term) -> None: _known_consts[name] = value +def traverse(f : Callable[[Term], Term], term : Term) -> Term: + """ + Traverse through the tree back-and-forth, aiming to run the given + function as thoroughly as possible to manipulate the term tree. + + :param f: The traversal function that replaces terms. + :type f: Callable[[Term], Term] + :param term: The term to traverse. + :type term: Term + :return: The result of the traversed term. + :rtype: Term + """ + return traverse_bottom_up(f=f, term=traverse_top_down(f=f, term=term)) + +def traverse_bottom_up(f : Callable[[Term], Term], term : Term) -> Term: + """ + Traverse a term from the bottom up, replacing values with whatever the + inserted function returns. + + :param f: The traversal function that replaces terms. + :type f: Callable[[Term], Term] + :param term: The term to traverse. + :type term: Term + :return: The result of the traversed term. + :rtype: Term + """ + match term: + case App(): + return f(App( + f=traverse_bottom_up(f=f, term=term.f), + x=traverse_bottom_up(f=f, term=term.x)), + ) + + case Const(): + return f(term) + + case Lambda(): + return term.replace_content( + traverse_bottom_up(f=f, term=term.out) + ) + + case Var(): + return f(term) + + case Term(): + return f(term) + +def traverse_top_down(f : Callable[[Term], Term], term : Term) -> Term: + """ + Traverse a term from the top down, replacing values with whatever the + inserted function returns. + + :param f: The traversal function that replaces terms. + :type f: Callable[[Term], Term] + :param term: The term to traverse. + :type term: Term + :return: The result of the traversed term. + :rtype: Term + """ + t = f(term) + + match t: + case App(): + return App( + f=traverse_top_down(f=f, term=t.f), + x=traverse_top_down(f=f, term=t.x), + ) + + case Const(): + return t + + case Lambda(): + return t.replace_content(traverse_top_down(f=f, term=t.out)) + + case Var(): + return t + + case Term(): + return t + class Term: """ Base class for all terms. """ + + def __eq__(self, other) -> bool: + """ + Determine whether two terms are equal. + """ + return str(self) == str(other) + + def __repr__(self) -> str: + """ + Create a representation of a term. + """ + return self.to_str(vars={}) def normalize(self) -> Term: - """ - Function to return a simplified version of the term. - """ - return self - - def reduce_on_equality(self, other : Term) -> tuple[Term, Term]: - """ - Reduce parts that the two items are equal on. - """ - return self, other - - def substitute(self, index : int, value : Term) -> Term: - """ - Substitute all variables of a given index number. + return normalize(term=self) - :param index: The variable's index. - :type index: int - :param value: The value to replace the variable with. - :type value: - """ - return self + def to_str(self, vars : dict[str, Var]) -> str: + return "" @dataclass(frozen=True) class App(Term): @@ -52,61 +179,26 @@ class App(Term): f : Term x : Term - def normalize(self) -> Term: - f = self.f.normalize() - x = self.x.normalize() - - default = App(f=f, x=x) - - match f: - case App(): - return default - - case Const(): - return default - - case Lambda(): - return f.resolve(x) - - case Term(): - return default - - case Var(): - return default - - def reduce_on_equality(self, other: Term) -> tuple[Term, Term]: - if not isinstance(other, App): - return self, other - - f1, f2 = self.f.normalize(), other.f.normalize() - x1, x2 = self.x.normalize(), other.x.normalize() - - match ( f1 == f2, x1 == x2 ): - case ( True, True ): - return Term(), Term() - - case ( True, False ): - return x1.reduce_on_equality(x2) - - case ( False, True ): - return f1.reduce_on_equality(f2) - - case ( False, False ): - return self, other - - def substitute(self, index : int, value : Term) -> Term: + def __repr__(self) -> str: """ - Substitute all variables of a given index number. - - :param index: The variable's index. - :type index: int - :param value: The value to replace the variable with. - :type value: + Create a representation of a term. """ - return App( - f=self.f.substitute(index=index, value=value), - x=self.x.substitute(index=index, value=value), - ) + return self.to_str(vars={}) + + def to_str(self, vars: dict[str, Var]) -> str: + f_str = self.f.to_str(vars=vars) + x_str = self.x.to_str(vars=vars) + + return f_str + " " + (f"({x_str})" if " " in x_str else x_str) + +A1 = lambda fn, a : App(f=fn, x=a) +A2 = lambda fn, a, b : App(f=A1(fn, a), x=b) +A3 = lambda fn, a, b, c : App(f=A2(fn, a, b), x=c) +A4 = lambda fn, a, b, c, d : App(f=A3(fn, a, b, c), x=d) +A5 = lambda fn, a, b, c, d, e : App(f=A4(fn, a, b, c, d), x=e) +A6 = lambda fn, a, b, c, d, e, f : App(f=A5(fn, a, b, c, d, e), x=f) +A7 = lambda fn, a, b, c, d, e, f, g : App(f=A6(fn, a, b, c, d, e, f), x=g) +A8 = lambda fn, a, b, c, d, e, f, g, h : App(f=A7(fn, a, b, c, d, e, f, g), x=h) @dataclass(frozen=True) class Const(Term): @@ -117,90 +209,201 @@ class Const(Term): name : str - def normalize(self) -> Term: - if self.name in _known_consts: - return copy.deepcopy(_known_consts.get(self.name, self)) - else: - return self + def __repr__(self) -> str: + """ + Create a representation of a term. + """ + return self.to_str(vars={}) -@dataclass(frozen=True) -class EqT(Term): - """ - Equality operator. Possibly the only function that is implemented into - the core of the term definitions. - """ + def to_str(self, vars: dict[str, Var]) -> str: + return self.name - lhs : Term - rhs : Term - - def normalize(self) -> Term: - l = self.lhs.normalize() - r = self.rhs.normalize() - - if l == r: - return Const("Bool.True") - else: - return Const("Bool.False") - -@dataclass(frozen=True) class Lambda(Term): """ Lambdas a nameless 1-ary functions. """ out : Term + var : Var - def normalize(self) -> Term: - return Lambda(out=self.out.normalize()) + def __init__(self, f : Callable[[Var], Term]) -> None: + self.var = Var() + self.out = f(self.var) + + def __repr__(self) -> str: + """ + Create a representation of a term. + """ + return self.to_str(vars={}) - def reduce_on_equality(self, other: Term) -> tuple[Term, Term]: - match other: - case Lambda(): - return self.out, other.out - case _: - return self, other - - def resolve(self, value : Term) -> Term: + def replace_content(self, term : Term) -> Lambda: """ - Resolve this lambda function by inserting a value. + Replace the content of the lambda function with the given term. + The new term may still contain the lambda's var as an argument. - :param value: The value to substitute. + :param term: The term to insert in a lambda function. + :type term: Term + :return: The new Lambda function. + :rtype: Lambda """ - return self.substitute(index=-1, value=value) + return Lambda( + lambda x : traverse_bottom_up( + f=lambda t : x if t is self.var else t, + term=term, + ) + ) - def substitute(self, index : int, value : Term) -> Term: + def substitute(self, value : Term) -> Term: """ Substitute all variables of a given index number. - :param index: The variable's index. - :type index: int :param value: The value to replace the variable with. - :type value: + :type value: Term + :return: A resolved lambda where the term has been substituted. + :rtype: Term """ - if index == -1: - # We're resolving this lambda function! - return self.out.substitute(index=index + 1, value=value) + return traverse_bottom_up( + f=lambda t : value if t is self.var else t, + term=self.out, + ) + + def to_str(self, vars: dict[str, Var]) -> str: + char = '' + + for c in USABLE_VAR_NAMES: + if c not in vars: + char = c + vars[c] = self.var + break else: - return Lambda(out=self.out.substitute(index=index + 1, value=value)) + raise ValueError( + f"Cannot represent a lambda function that's over {len(USABLE_VAR_NAMES)} layers deep!" + ) + + s = self.out.to_str(vars=vars) + + del vars[char] + return "λ" + char + "." + (f"({s})" if " " in s else s) + +L1 = lambda f : Lambda(lambda x : f(x)) +L2 = lambda f : Lambda(lambda x : L1(lambda y : f(x, y))) +L3 = lambda f : Lambda(lambda x : L2(lambda y, z : f(x, y, z))) +L4 = lambda f : Lambda(lambda x : L3(lambda y, z, a : f(x, y, z, a))) +L5 = lambda f : Lambda(lambda x : L4(lambda y, z, a, b : f(x, y, z, a, b))) +L6 = lambda f : Lambda(lambda x : L5(lambda y, z, a, b, c : f(x, y, z, a, b, c))) +L7 = lambda f : Lambda(lambda x : L6(lambda y, z, a, b, c, d : f(x, y, z, a, b, c, d))) +L8 = lambda f : Lambda(lambda x : L7(lambda y, z, a, b, c, d, e : f(x, y, z, a, b, c, d, e))) @dataclass(frozen=True) class Var(Term): + """ A variable is a value that can be substituted by a lambda function. + + Each lambda function stores a unique var, which can then point to a new + structure later on. """ - index : int - - def substitute(self, index : int, value : Term) -> Term: + def __repr__(self) -> str: """ - Substitute all variables of a given index number. - - :param index: The variable's index. - :type index: int - :param value: The value to replace the variable with. - :type value: + Create a representation of a term. """ - if self.index == index: - return copy.deepcopy(value) + return self.to_str(vars={}) + + def to_str(self, vars: dict[str, Var]) -> str: + for i, v in vars.items(): + if v is self: + return i else: - return self + return "[ERROR:UNKNOWN_VAR]" + +if __name__ == "__main__": + print("REPRESENTATIONS") + print(30 * "=") + + # x + print(Const("x")) + + # λx.(f x) + print(Lambda(lambda a : App(f=Const("f"), x=a))) + + # λx.(λy.(x y)) + print(Lambda(lambda b : Lambda(lambda c : App(f=b, x=c)))) + + # Nat.Succ (Nat.Succ Nat.Zero) + print(App(f=Const("Nat.Succ"), x=App(f=Const("Nat.Succ"), x=Const("Nat.Zero")))) + + + print("\nNORMALIZATIONS") + print(30 * "=") + + # foo + a = App(f=Lambda(lambda x : x), x=Const("foo")) + print(a) + print(a.normalize()) + + # f x + b = App( + f=App( + f=Lambda( + lambda f : Lambda( + lambda x : App( + f=f, x=x + ) + ) + ), + x=Const("f"), + ), + x= Const("x"), + ) + print(b) + print(b.normalize()) + + # a b c + c = App( + f=App( + f=App( + f=Lambda( + lambda x : Lambda( + lambda y : Lambda( + lambda z : App( + f=App(f=x, x=y), x=z + ) + ) + ) + ), + x=Const("a"), + ), + x=Const("b"), + ), + x=Const("c"), + ) + print(c) + print(c.normalize()) + + # + d = L3(lambda x, y, z : A2(x, y, z)) + print(d) + print(d.normalize()) + + + print("\nSHORTHAND NOTATION") + print(30 * "=") + + # λx.(λy.(λz.(x y z)) + e = L3(lambda a, b, c : App(f=App(f=a, x=b), x=c)) + print(e) + + + # λx.(λy.(λz.(x y z)) + f = L3(lambda a, b, c : A3(L3(lambda a, b, c : A2(a, b, c)), a, b, c)) + print(f) + print(f.normalize()) + assert e == f.normalize() + + # not + bool_t = L2(lambda x, y : x).normalize() + bool_f = L2(lambda x, y : y).normalize() + g = L1(lambda b : A2(b, bool_f, bool_t)) + print(g) + print(g.normalize())