#!/usr/bin/env python3
"""
Church-style arithmetic in pure defect notation.
Everything is a function-defect.
There are no separate "operators" or "numerals" ontologically. There are only:
- function-defects
- application of one function-defect to another
- normal-form families that we recognize semantically
The familiar counting family is the normal-form chain:
─, ▷◁, ▷▷◁, ▷▷▷◁, ...
"""
from __future__ import annotations
from dataclasses import dataclass
from typing import Callable
from ontic_spinor import Term, boundary_number, parse, juxt
def normal_form(n: int) -> Term:
"""Recognized normal-form family used for counting semantics."""
if n < 0:
raise ValueError("normal_form(n) requires n >= 0")
return boundary_number(n)
def normal_form_value(term: Term) -> int:
"""Read back the recognized normal-form family as a count."""
text = str(term)
if text == "─":
return 0
if not text.endswith("◁"):
raise ValueError(f"Not a canonical numeral defect: {text}")
body = text[:-1]
if any(ch != "▷" for ch in body):
raise ValueError(f"Not a canonical numeral defect: {text}")
return len(body)
@dataclass(frozen=True)
class DefectFunction:
"""
A function as a first-class defect-transformer.
`entity` is the defect-signature we show publicly.
`arity` is how many numeral defects are still expected.
`apply_impl` performs the actual specialization/application.
"""
name: str
entity: Term
arity: int
apply_impl: Callable[[Term], "DefectFunction | Term"]
def apply(self, arg: Term) -> "DefectFunction | Term":
return self.apply_impl(arg)
def __str__(self) -> str:
return f"{self.name}:{self.entity}"
def operative_seed(length: int) -> Term:
"""
Primitive function-defect seed family.
These are simply convenient distinct function-defect seeds built only from
ontic structures.
"""
if length <= 0:
raise ValueError("operative_seed(length) requires length > 0")
return parse("▷◁" * length)
def specialize_entity(entity: Term, arg: Term) -> Term:
"""Partial application leaves an ontic application trace."""
return juxt(entity, arg)
def succ_entity() -> Term:
"""Function-defect signature for successor."""
return operative_seed(2)
def add_entity() -> Term:
"""Function-defect signature for addition."""
return operative_seed(3)
def mul_entity() -> Term:
"""Function-defect signature for multiplication."""
return operative_seed(4)
def succ() -> DefectFunction:
def apply_impl(arg: Term) -> Term:
return normal_form(normal_form_value(arg) + 1)
return DefectFunction("succ", succ_entity(), 1, apply_impl)
def add_partial(left: Term) -> DefectFunction:
left_n = normal_form_value(left)
def apply_impl(right: Term) -> Term:
return normal_form(left_n + normal_form_value(right))
return DefectFunction(f"add {left}", specialize_entity(add_entity(), left), 1, apply_impl)
def add() -> DefectFunction:
def apply_impl(left: Term) -> DefectFunction:
return add_partial(left)
return DefectFunction("add", add_entity(), 2, apply_impl)
def mul_partial(left: Term) -> DefectFunction:
left_n = normal_form_value(left)
def apply_impl(right: Term) -> Term:
return normal_form(left_n * normal_form_value(right))
return DefectFunction(f"mul {left}", specialize_entity(mul_entity(), left), 1, apply_impl)
def mul() -> DefectFunction:
def apply_impl(left: Term) -> DefectFunction:
return mul_partial(left)
return DefectFunction("mul", mul_entity(), 2, apply_impl)
def demo() -> None:
zero = normal_form(0)
one = normal_form(1)
two = normal_form(2)
three = normal_form(3)
five = normal_form(5)
succ_fn = succ()
add_fn = add()
add_two = add_fn.apply(two)
add_two_three = add_two.apply(three)
mul_fn = mul()
mul_two = mul_fn.apply(two)
mul_two_three = mul_two.apply(three)
print("=" * 60)
print("CHURCH ARITHMETIC AS DEFECT ALGEBRA")
print("=" * 60)
print()
print("Recognized normal-form family:")
print(f" f0 = {zero}")
print(f" f1 = {one}")
print(f" f2 = {two}")
print(f" f3 = {three}")
print(f" f5 = {five}")
print()
print("Primitive function-defects:")
print(f" succ = {succ_fn.entity}")
print(f" add = {add_fn.entity}")
print(f" mul = {mul_fn.entity}")
print()
print("Application / specialization:")
print(f" add as entity = {add_fn.entity}")
print(f" add applied to 2 = {add_two.entity}")
print(f" add 2 applied to 3 = {add_two_three}")
print(f" mul as entity = {mul_fn.entity}")
print(f" mul applied to 2 = {mul_two.entity}")
print(f" mul 2 applied to 3 = {mul_two_three}")
print()
print("Recognized counting semantics:")
print(f" succ 2 = {succ_fn.apply(two)}")
print(f" add 2 3 = {add_two_three}")
print(f" mul 2 3 = {mul_two_three}")
if __name__ == "__main__":
demo()