improve BetaNormalisingVisitor and Substitutions

This commit modifies BetaNormalisingVisitor to yield alpha conversions,
which required refactoring the Visitors used for substitution

Author: Deric-W

README.md

@@ -11,6 +11,18 @@ and nest them to create more complex lambda terms.
 You can also use the `visitors` subpackage to define your own operations on terms or
 use predefined ones from the `terms` subpackage.
 
+## Notice
+
+This package is intended to be used for educational purposes and is not optimized for speed.
+
+Furthermore, it expects all terms to be finite, which means the absense of cycles.
+
+This results in the Visitor for term normalisation included in this package (`BetaNormalisingVisitor`)
+having problems when handling terms which are passed a reference to themselves during evaluation,
+which is the case for all recursive functions.
+
+`RecursionError` may be raised if the visitors get passed an infinite term.
+
 ## Requirements
 
 Python >= 3.10 is required to use this package.

lambda_calculus/__init__.py

@@ -4,7 +4,7 @@
 
 from .terms import Variable, Abstraction, Application
 
-__version__ = "1.11.0"
+__version__ = "2.0.0"
 __author__  = "Eric Niklas Wolf"
 __email__   = "[email protected]"
 __all__ = (

lambda_calculus/terms/__init__.py

@@ -9,7 +9,8 @@
 from typing import TypeVar
 from .. import visitors
 from ..errors import CollisionError
-from ..visitors import substitution, walking
+from ..visitors import walking
+from ..visitors.substitution import checked
 
 __all__ = (
     "Term",
@@ -63,7 +64,7 @@ def apply_to(self, *arguments: Term[V]) -> Application[V]:
 
     def substitute(self, variable: V, value: Term[V]) -> Term[V]:
         """substitute a free variable with a Term, possibly raising a CollisionError"""
-        return self.accept(substitution.SubstitutingVisitor(variable, value))
+        return self.accept(checked.CheckedSubstitution.from_substitution(variable, value))
 
     def is_combinator(self) -> bool:
         """return if this Term has no free variables"""

lambda_calculus/visitors/__init__.py

@@ -4,12 +4,13 @@
 
 from __future__ import annotations
 from abc import ABC, abstractmethod
-from typing import TypeVar, Generic
+from typing import TypeVar, Generic, final
 from .. import terms
 
 __all__ = (
     "Visitor",
     "BottomUpVisitor",
+    "DeferrableVisitor",
     "substitution",
     "normalisation",
     "walking"
@@ -27,14 +28,15 @@ class Visitor(ABC, Generic[T, V]):
 
     __slots__ = ()
 
+    @final
     def visit(self, term: terms.Term[V]) -> T:
         """visit a term"""
         return term.accept(self)
 
     @abstractmethod
     def visit_variable(self, variable: terms.Variable[V]) -> T:
         """visit a Variable term"""
-        raise NotADirectoryError()
+        raise NotImplementedError()
 
     @abstractmethod
     def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> T:
@@ -52,13 +54,15 @@ class BottomUpVisitor(Visitor[T, V]):
 
     __slots__ = ()
 
+    @final
     def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> T:
         """visit an Abstraction term"""
         return self.ascend_abstraction(
             abstraction,
             abstraction.body.accept(self)
         )
 
+    @final
     def visit_application(self, application: terms.Application[V]) -> T:
         """visit an Application term"""
         return self.ascend_application(
@@ -76,3 +80,19 @@ def ascend_abstraction(self, abstraction: terms.Abstraction[V], body: T) -> T:
     def ascend_application(self, application: terms.Application[V], abstraction: T, argument: T) -> T:
         """visit an Application term after visiting its abstraction and argument"""
         raise NotImplementedError()
+
+
+class DeferrableVisitor(Visitor[T, V]):
+    """ABC for visitors which can visit terms top down lazyly"""
+
+    __slots__ = ()
+
+    @abstractmethod
+    def defer_abstraction(self, abstraction: terms.Abstraction[V]) -> tuple[T, DeferrableVisitor[T, V] | None]:
+        """visit an Abstraction term and return the visitor used to visit its body"""
+        raise NotImplementedError()
+
+    @abstractmethod
+    def defer_application(self, application: terms.Application[V]) -> tuple[T, DeferrableVisitor[T, V] | None, DeferrableVisitor[T, V] | None]:
+        """visit an Application term and return the visitors used to visit its abstraction and argument"""
+        raise NotImplementedError()

lambda_calculus/visitors/normalisation.py

@@ -4,65 +4,84 @@
 
 from __future__ import annotations
 from collections.abc import Iterator
-from typing import TypeVar
+from enum import Enum, unique
+from typing import TypeVar, final, Generator, TypeAlias
 from .. import terms
 from . import Visitor
-from .substitution import CountingSubstitutingVisitor
+from .substitution.renaming import CountingSubstitution
 
 __all__ = (
+    "Conversion",
     "BetaNormalisingVisitor",
 )
 
 V = TypeVar("V")
 
+Step: TypeAlias = tuple["Conversion", terms.Term[str]]
 
-class BetaNormalisingVisitor(Visitor[Iterator[terms.Term[str]], str]):
+
+@unique
+class Conversion(Enum):
+    """Conversion performed by normalisation"""
+    ALPHA = 0
+    BETA = 1
+
+
+@final
+class BetaNormalisingVisitor(Visitor[Iterator[Step], str]):
     """
     Visitor which transforms a term into its beta normal form,
-    yielding intermediate results until it is reached
+    yielding intermediate steps until it is reached
     """
 
     __slots__ = ()
 
     def skip_intermediate(self, term: terms.Term[str]) -> terms.Term[str]:
         """return the beta normal form directly"""
         result = term
-        for intermediate in term.accept(self):
+        for _, intermediate in term.accept(self):
             result = intermediate
         return result
 
-    def visit_variable(self, variable: terms.Variable[str]) -> Iterator[terms.Variable[str]]:
+    def visit_variable(self, variable: terms.Variable[str]) -> Iterator[Step]:
         """visit a Variable term"""
         return iter(())
 
-    def visit_abstraction(self, abstraction: terms.Abstraction[str]) -> Iterator[terms.Abstraction[str]]:
+    def visit_abstraction(self, abstraction: terms.Abstraction[str]) -> Iterator[Step]:
         """visit an Abstraction term"""
         results = abstraction.body.accept(self)
-        return map(lambda b: terms.Abstraction(abstraction.bound, b), results)
+        return map(lambda s: (s[0], terms.Abstraction(abstraction.bound, s[1])), results)
+
+    def beta_reducation(self, abstraction: terms.Abstraction[str], argument: terms.Term[str]) -> Generator[Step, None, terms.Term[str]]:
+        """perform beta reduction of an application"""
+        conversions = CountingSubstitution.from_substitution(abstraction.bound, argument).trace()
+        reduced = yield from map(
+            lambda body: (
+                Conversion.ALPHA,
+                terms.Application(terms.Abstraction(abstraction.bound, body), argument)
+            ),
+            abstraction.body.accept(conversions)    # type: ignore
+        )
+        yield (Conversion.BETA, reduced)
+        return reduced      # type: ignore
 
-    def visit_application(self, application: terms.Application[str]) -> Iterator[terms.Term[str]]:
+    def visit_application(self, application: terms.Application[str]) -> Iterator[Step]:
         """visit an Application term"""
-        match application.abstraction:
-            # normal order dictates we reduce leftmost outermost redex first
-            case terms.Abstraction(bound, body):
-                reduced = body.accept(CountingSubstitutingVisitor(bound, application.argument))
-                yield reduced
-                yield from reduced.accept(self)
-            case _:
-                # try to reduce the abstraction until this is a redex
-                abstraction = application.abstraction
-                for transformation in application.abstraction.accept(self):
-                    yield terms.Application(transformation, application.argument)
-                    match transformation:
-                        case terms.Abstraction(bound, body):
-                            reduced = body.accept(
-                                CountingSubstitutingVisitor(bound, application.argument)
-                            )
-                            yield reduced
-                            yield from reduced.accept(self)
-                            return
-                        case _:
-                            abstraction = transformation
-                # no redex, continue with argument
-                transformations = application.argument.accept(self)
-                yield from map(lambda a: terms.Application(abstraction, a), transformations)
+        if isinstance(application.abstraction, terms.Abstraction):
+            # normal order dictates we reduce the leftmost outermost redex first
+            reduced = yield from self.beta_reducation(application.abstraction, application.argument)
+            yield from reduced.accept(self)
+        else:
+            # try to reduce the abstraction until this is a redex
+            abstraction = application.abstraction
+            for conversion, transformation in application.abstraction.accept(self):
+                yield (conversion, terms.Application(transformation, application.argument))
+                if isinstance(transformation, terms.Abstraction):
+                    reduced = yield from self.beta_reducation(transformation, application.argument)
+                    yield from reduced.accept(self)
+                    return
+                else:
+                    abstraction = transformation
+            # no redex, continue with argument
+            transformations = application.argument.accept(self)
+            yield from map(lambda s: (s[0], terms.Application(abstraction, s[1])), transformations)