add arithmetic lambda terms

Author: Deric-W

README.md

@@ -5,7 +5,8 @@ The `lambda_calculus` package contains classes which implement basic operations
 To use it, simply import the classes `Variable`, `Abstraction` and `Application` from this package
 and nest them to create more complex lambda terms.
 
-You can also use the `visitors` subpackage to define your own operations on terms.
+You can also use the `visitors` subpackage to define your own operations on terms or
+use predefined ones from the `terms` subpackage.
 
 ## Requirements
 

lambda_calculus/__init__.py

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

lambda_calculus/terms/__init__.py

@@ -15,7 +15,8 @@
     "Term",
     "Variable",
     "Abstraction",
-    "Application"
+    "Application",
+    "arithmetic"
 )
 
 T = TypeVar("T")

lambda_calculus/terms/arithmetic.py

@@ -0,0 +1,102 @@
+#!/usr/bin/python3
+
+"""Implementations of natural numbers and arithmetic operators"""
+
+from . import Term, Variable, Abstraction, Application
+
+__all__ = (
+    "SUCCESSOR",
+    "PREDECESSOR",
+    "ADD",
+    "SUBTRACT",
+    "MULTIPLY",
+    "POWER",
+    "number"
+)
+
+SUCCESSOR = Abstraction.curried(
+    ("n", "f", "x"),
+    Application(
+        Variable("f"),
+        Application.with_arguments(
+            Variable("n"),
+            (Variable("f"), Variable("x"))
+        )
+    )
+)
+
+PREDECESSOR = Abstraction.curried(
+    ("n", "f", "x"),
+    Application.with_arguments(
+        Variable("n"),
+        (
+            Abstraction.curried(
+                ("g", "h"),
+                Application(
+                    Variable("h"),
+                    Application(
+                        Variable("g"),
+                        Variable("f")
+                    )
+                )
+            ),
+            Abstraction("u", Variable("x")),
+            Abstraction("u", Variable("u")),
+        )
+    )
+)
+
+ADD = Abstraction.curried(
+    ("m", "n", "f", "x"),
+    Application.with_arguments(
+        Variable("m"),
+        (
+            Variable("f"),
+            Application.with_arguments(
+                Variable("n"),
+                (Variable("f"), Variable("x"))
+            )
+        )
+    )
+)
+
+SUBTRACT = Abstraction.curried(
+    ("m", "n"),
+    Application.with_arguments(
+        Variable("n"),
+        (PREDECESSOR, Variable("m"))
+    )
+)
+
+MULTIPLY = Abstraction.curried(
+    ("m", "n", "f"),
+    Application(
+        Variable("m"),
+        Application(
+            Variable("n"),
+            Variable("f")
+        )
+    )
+)
+
+POWER = Abstraction.curried(
+    ("b", "e"),
+    Application(
+        Variable("e"),
+        Variable("b")
+    )
+)
+
+
+def number(n: int) -> Abstraction[str]:
+    """return n encoded in lambda terms"""
+    if n < 0:
+        raise ValueError("number is not natural")
+    f = Variable("f")
+    body: Term[str] = Variable("x")
+    for _ in range(n):
+        body = Application(f, body)
+    return Abstraction.curried(
+        ("f", "x"),
+        body
+    )

pyproject.toml

@@ -1,6 +1,6 @@
 [project]
 name = "lambda_calculus"
-version = "1.7.1"
+version = "1.8.0"
 description = "Implementation of the Lambda calculus"
 requires-python = ">=3.10"
 keywords = []

tests/terms/test_arithmetic.py

@@ -0,0 +1,150 @@
+#!/usr/bin/python3
+
+"""Tests for arithmetic terms"""
+
+from unittest import TestCase
+from lambda_calculus.visitors.normalisation import BetaNormalisingVisitor
+from lambda_calculus.terms import Application, arithmetic
+
+
+class OrderingTest(TestCase):
+    """Test for ordering functions"""
+
+    visitor: BetaNormalisingVisitor
+
+    def setUp(self) -> None:
+        """create a visitor"""
+        self.visitor = BetaNormalisingVisitor()
+
+    def test_successor(self) -> None:
+        """test successor term"""
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application(arithmetic.SUCCESSOR, arithmetic.number(8))
+            ),
+            arithmetic.number(9)
+        )
+
+    def test_predecessor(self) -> None:
+        """test predecessor term"""
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application(arithmetic.PREDECESSOR, arithmetic.number(8))
+            ),
+            arithmetic.number(7)
+        )
+
+    def test_predecessor_zero(self) -> None:
+        """test predecessor of zero"""
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application(arithmetic.PREDECESSOR, arithmetic.number(0))
+            ),
+            arithmetic.number(0)
+        )
+
+
+class CalculationsTest(TestCase):
+    """Test for calculations with natural numbers"""
+
+    visitor: BetaNormalisingVisitor
+
+    def setUp(self) -> None:
+        """create a visitor"""
+        self.visitor = BetaNormalisingVisitor()
+
+    def test_add(self) -> None:
+        """test addition term"""
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application.with_arguments(
+                    arithmetic.ADD,
+                    (arithmetic.number(3), arithmetic.number(5))
+                )
+            ),
+            arithmetic.number(8)
+        )
+
+    def test_subtract(self) -> None:
+        """test subtraction term"""
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application.with_arguments(
+                    arithmetic.SUBTRACT,
+                    (arithmetic.number(10), arithmetic.number(3))
+                )
+            ),
+            arithmetic.number(7)
+        )
+
+    def test_subtract_greater(self) -> None:
+        """test subtraction below zero"""
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application.with_arguments(
+                    arithmetic.SUBTRACT,
+                    (arithmetic.number(10), arithmetic.number(13))
+                )
+            ),
+            arithmetic.number(0)
+        )
+
+    def test_multiply(self) -> None:
+        """test multiplication term"""
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application.with_arguments(
+                    arithmetic.MULTIPLY,
+                    (arithmetic.number(5), arithmetic.number(2))
+                )
+            ),
+            arithmetic.number(10)
+        )
+
+    def test_power(self) -> None:
+        """test power term"""
+        # alpha conversion needed
+        nine = arithmetic.number(9)
+        nine = nine.replace(body=nine.body.alpha_conversion("x1"))
+        nine = nine.alpha_conversion("x")
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application.with_arguments(
+                    arithmetic.POWER,
+                    (arithmetic.number(3), arithmetic.number(2))
+                )
+            ),
+            nine
+        )
+
+    def test_power_zero(self) -> None:
+        """test power zero"""
+        one = self.visitor.skip_intermediate(
+            Application.with_arguments(
+                arithmetic.POWER,
+                (arithmetic.number(5), arithmetic.number(0))
+            )
+        )
+        # eta conversion needed
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application.with_arguments(
+                    arithmetic.ADD,
+                    (one, arithmetic.number(3))
+                )
+            ),
+            arithmetic.number(4)
+        )
+        # alpha conversion needed
+        zero = arithmetic.number(0)
+        zero = zero.replace(body=zero.body.alpha_conversion("x1"))
+        zero = zero.alpha_conversion("x")
+        self.assertEqual(
+            self.visitor.skip_intermediate(
+                Application.with_arguments(
+                    arithmetic.POWER,
+                    (arithmetic.number(0), arithmetic.number(5))
+                )
+            ),
+            zero
+        )