Same orchard, same ground truth — but axioms now use ?... splat patterns for variadic operations: sum-all, count-gt, all-gt. No more nested binary ops: (sum-all a b c d) replaces (+ (+ (+ a b) c) d).
"""
Demo: Apple Arithmetic with Variadic Splats (?...).
Same orchard, same ground truth — but axioms now use ?... splat
patterns for variadic operations: sum-all, count-gt, all-gt.
No more nested binary ops: (sum-all a b c d) replaces (+ (+ (+ a b) c) d).
"""
import json
import logging
import os
import sys
from parseltongue import load_main
def provenance(system, name):
print(json.dumps(system.provenance(str(name)), indent=2))
return True
def consistency(system):
report = system.consistency()
print(f" {report}")
return report.consistent
def verify(system, name):
system.verify_manual(str(name))
return True
def dump_env(system):
env = system.engine.env
print(f" Environment has {len(env)} entries: {list(env.keys()) if env else '(empty)'}")
return True
def state(system):
print(f" {system}")
return True
def list_axioms(system):
for ax in system.list_axioms():
print(f" {ax}")
return True
def list_terms(system):
for t in system.list_terms():
print(f" {t}")
return True
def list_theorems(system):
for t in system.list_theorems():
print(f" {t}")
return True
def print_theorem(system, name):
name = str(name)
if name in system.theorems:
print(f" {system.theorems[name]}")
return True
def print_facts(system):
for f in system.list_facts():
print(f" {f}")
return True
def pltg_print(_system, *args):
print(*[str(a).replace("\\n", "\n") for a in args])
return True
if __name__ == "__main__":
plog = logging.getLogger("parseltongue")
plog.setLevel(logging.WARNING)
handler = logging.StreamHandler(sys.stdout)
handler.setFormatter(logging.Formatter(" [%(levelname)s] %(message)s"))
plog.addHandler(handler)
os.chdir(os.path.dirname(__file__))
load_main(
"demo.pltg",
{
"dump-env": dump_env,
"print": pltg_print,
"provenance": provenance,
"consistency": consistency,
"verify": verify,
"state": state,
"list-axioms": list_axioms,
"list-terms": list_terms,
"list-theorems": list_theorems,
"print-theorem": print_theorem,
"print-facts": print_facts,
},
initial_env={},
overridable=True,
)
; ==========================================================
; Parseltongue DSL — Apple Arithmetic with Variadic Splats
; ==========================================================
; Like apples_pltg but uses ?... splat patterns for variadic
; axioms: sum-all, count-gt, all-gt. No more nested binary ops.
(print "============================================================")
(print "Apple Arithmetic with Variadic Splats (?...)")
(print "============================================================")
; --- Phase 0: Load source documents ---
(print "\n--- Phase 0: Load source documents ---")
(load-document "Counting Observations" "resources/counting_observations.txt")
(load-document "Eden Inventory" "resources/eden_inventory.txt")
; --- Phase 1: Primitives ---
(print "\n--- Phase 1: Introduce primitive symbols ---")
(import (quote src.primitives))
(defterm local-zero src.primitives.zero :origin "import")
(defterm local-succ src.primitives.succ :origin "import")
; --- Phase 2: Axioms (Peano + splat reductions) ---
(print "\n--- Phase 2: Axioms ---")
(import (quote src.axioms))
; Local aliases for readable derives
(defterm = src.axioms.= :origin "import")
(defterm + src.axioms.+ :origin "import")
(defterm > src.axioms.> :origin "import")
(defterm and src.axioms.and :origin "import")
(defterm sum-all src.axioms.sum-all :origin "import")
(defterm count-gt src.axioms.count-gt :origin "import")
(defterm all-gt src.axioms.all-gt :origin "import")
(print " Axioms:")
(list-axioms)
; --- Phase 3: Harvest data ---
(print "\n--- Phase 3: Harvest data ---")
(import (quote src.morning))
(import (quote src.afternoon))
; --- Phase 4: Variadic totals via sum-all ---
; OLD way: (+ (+ eve-morning adam-morning) (+ serpent-afternoon eve-afternoon))
; NEW way: just list them all
(print "\n--- Phase 4: Variadic totals (sum-all) ---")
(defterm morning-total (sum-all src.morning.eve-morning src.morning.adam-morning)
:evidence (evidence "Eden Inventory"
:quotes ("Combined morning harvest was 🍎🍎🍎🍎🍎🍎🍎🍎 apples")
:explanation "Sum of all morning picks"))
(defterm afternoon-total (sum-all src.afternoon.serpent-afternoon src.afternoon.eve-afternoon)
:evidence (evidence "Eden Inventory"
:quotes ("Combined afternoon harvest was 🍎🍎🍎🍎🍎🍎 apples")
:explanation "Sum of all afternoon picks"))
; Grand total: four pickers in one expression
(defterm daily-total
(sum-all src.morning.eve-morning src.morning.adam-morning
src.afternoon.serpent-afternoon src.afternoon.eve-afternoon)
:evidence (evidence "Eden Inventory"
:quotes ("Total harvest for the day was 🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎 apples")
:explanation "Grand total = all four picks summed at once via sum-all"))
(defterm eve-daily (sum-all src.morning.eve-morning src.afternoon.eve-afternoon)
:evidence (evidence "Eden Inventory"
:quotes ("Eve's daily total is 🍎🍎🍎🍎🍎 apples")
:explanation "Eve's combined morning + afternoon"))
(print " Terms:")
(list-terms)
; --- Phase 5: Variadic counting (count-gt) ---
; How many pickers got more than 3 apples in a single shift?
; Threshold: SSS0 (3 apples)
(print "\n--- Phase 5: Count big harvests (count-gt) ---")
(defterm threshold (succ (succ (succ zero)))
:origin "3 apples — a good haul")
(defterm big-harvest-count
(count-gt threshold
src.morning.eve-morning
src.morning.adam-morning
src.afternoon.serpent-afternoon
src.afternoon.eve-afternoon)
:evidence (evidence "Eden Inventory"
:quotes ("Adam picked 🍎🍎🍎🍎🍎 apples from the west grove"
"Serpent picked 🍎🍎🍎🍎 apples from the south grove")
:explanation "Count shifts with more than 3: Adam morning (5>3), Serpent afternoon (4>3) = 2"))
; --- Phase 6: Variadic check (all-gt) ---
; Did everyone pick at least 1 apple? Threshold: S0 (1 apple)
(print "\n--- Phase 6: All above minimum? (all-gt) ---")
(defterm minimum (succ zero)
:origin "1 apple — minimum expected")
(defterm all-picked-enough
(all-gt minimum
src.morning.eve-morning
src.morning.adam-morning
src.afternoon.serpent-afternoon
src.afternoon.eve-afternoon)
:evidence (evidence "Eden Inventory"
:quotes ("Eve picked 🍎🍎🍎 apples from the east grove"
"Adam picked 🍎🍎🍎🍎🍎 apples from the west grove"
"Serpent picked 🍎🍎🍎🍎 apples from the south grove"
"Eve picked 🍎🍎 more apples from the east grove")
:explanation "All four shifts produced more than 1 apple"))
; --- Phase 7: Derives using splat axioms ---
(print "\n--- Phase 7: Derives ---")
(derive morning-sum-correct
(= (sum-all src.morning.eve-morning src.morning.adam-morning) morning-total)
:using (= + sum-all
src.morning.eve-morning src.morning.adam-morning
morning-total src.axioms.sum-all-base src.axioms.sum-all-step
src.axioms.eq-reflexive))
(derive all-above-minimum
(= (all-gt minimum
src.morning.eve-morning src.morning.adam-morning
src.afternoon.serpent-afternoon src.afternoon.eve-afternoon)
true)
:using (= > and all-gt
minimum src.morning.eve-morning src.morning.adam-morning
src.afternoon.serpent-afternoon src.afternoon.eve-afternoon
src.axioms.all-gt-base src.axioms.all-gt-step
src.axioms.eq-reflexive))
(print " Theorems:")
(print-theorem "morning-sum-correct")
(print-theorem "all-above-minimum")
; --- Phase 8: Diff — what if Eve tried the forbidden apple? ---
(print "\n--- Phase 8: Diff — what if Eve tried the forbidden apple? ---")
(defterm eve-morning-alt (succ (succ zero))
:origin "Hypothetical: Eve tried the forbidden apple — SS0 instead of SSS0")
(diff eve-check
:replace src.morning.eve-morning
:with eve-morning-alt)
; --- Phase 9: Provenance & consistency ---
(print "\n--- Phase 9: Provenance ---")
(provenance "morning-sum-correct")
(print "\n--- Phase 10: Consistency ---")
(consistency)
(print "\n Resolving unverified items...")
(verify "eve-morning-alt")
(verify "threshold")
(verify "minimum")
(verify "src.axioms.eq-reflexive")
(verify "src.primitives.=")
(print "\n After verification:")
(consistency)
; --- Summary ---
(print "\n============================================================")
(state)
(print "\n============================================================")
(print "Same orchard, same apples — but now with variadic axioms.")
(print "(sum-all a b c d) instead of (+ (+ (+ a b) c) d)")
(print "(count-gt threshold a b c) counts how many exceed it")
(print "(all-gt minimum a b c) checks everyone meets it")
(print "All powered by ?... splat pattern matching.")
(print "============================================================")
Field Notes: Observations on Shuffling Apples
Researcher: E. Peano, Fruit Laboratory
Observation 1: Piling Up
When placing apples into a basket one by one, every pile is reached by
adding one more apple to the previous pile. We decided to mark an empty
basket as "zero".
Observation 2: Combining Collections
When we pour one basket into another, the resulting pile is the union of
both. Combining 🍎🍎🍎 apples with 🍎🍎 apples always gives 🍎🍎🍎🍎🍎 apples.
We repeated this trial many times with identical results.
Observation 3: Order Independence
The order of combining does not matter — pouring basket A into basket B gives
the same pile as pouring basket B into basket A. We confirmed this by
swapping the pour direction across all trials.
Observation 4: Adding Nothing
Adding nothing to a basket does not change the pile. A basket of apples
still has the same apples after we pretend to pour an empty basket into it.
Observation 5: Comparing Collections
The basket with more apples is always heavier. If basket A has 🍎🍎🍎🍎🍎 and
basket B has 🍎🍎🍎, then basket A has more. The difference is found by
removing apples from the larger pile until it matches the smaller.
Observation 6: Swap Invariance
Swapping all apples between two equal baskets does not change either pile.
If both baskets have 🍎🍎🍎🍎 apples, after swapping they still each have 🍎🍎🍎🍎.
Observation 7: Equal Groups
Having several baskets each holding the same pile of apples is the same as
adding that pile repeatedly. Multiplication is a shortcut for combining
equal groups.
Garden of Eden — Daily Harvest Log
Date: October 15
Morning Shift
Eve picked 🍎🍎🍎 apples from the east grove.
Adam picked 🍎🍎🍎🍎🍎 apples from the west grove.
Combined morning harvest was 🍎🍎🍎🍎🍎🍎🍎🍎 apples.
Adam picked more apples than Eve in the morning.
Afternoon Shift
Serpent picked 🍎🍎🍎🍎 apples from the south grove.
Eve picked 🍎🍎 more apples from the east grove.
Combined afternoon harvest was 🍎🍎🍎🍎🍎🍎 apples.
Daily Summary
Eve's daily total is 🍎🍎🍎🍎🍎 apples.
Total harvest for the day was 🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎 apples.
Adam had the highest individual count with 🍎🍎🍎🍎🍎 apples.
The morning shift outproduced the afternoon by 🍎🍎 apples.
; Afternoon harvest (same as apples_pltg)
(defterm serpent-afternoon (succ (succ (succ (succ zero))))
:evidence (evidence "Eden Inventory"
:quotes ("Serpent picked 🍎🍎🍎🍎 apples from the south grove")
:explanation "Serpent's afternoon count: SSSS0"))
(defterm eve-afternoon (succ (succ zero))
:evidence (evidence "Eden Inventory"
:quotes ("Eve picked 🍎🍎 more apples from the east grove")
:explanation "Eve's afternoon count: SS0"))
; Phase 2: Axioms — Peano arithmetic + variadic splat reductions
(import (quote primitives))
(defterm zero src.primitives.zero :origin "import")
(defterm succ src.primitives.succ :origin "import")
(defterm = src.primitives.= :origin "import")
(defterm + src.primitives.+ :origin "import")
(defterm - src.primitives.- :origin "import")
(defterm > src.primitives.> :origin "import")
(defterm * primitives.* :origin "import")
(defterm and src.primitives.and :origin "import")
; --- Classic Peano axioms ---
(axiom eq-reflexive (= ?x ?x)
:evidence (evidence "Counting Observations"
:quotes ("If both baskets have 🍎🍎🍎🍎 apples, after swapping they still each have 🍎🍎🍎🍎")
:explanation "Equality is reflexive: any pile equals itself"))
(axiom add-identity (= (+ ?n zero) ?n)
:evidence (evidence "Counting Observations"
:quotes ("Adding nothing to a basket does not change the pile")
:explanation "Additive identity: n + 0 = n"))
(axiom add-succ (= (+ ?n (succ ?m)) (succ (+ ?n ?m)))
:evidence (evidence "Counting Observations"
:quotes ("every pile is reached by adding one more apple to the previous pile")
:explanation "Addition step: n + S(m) = S(n + m)"))
(axiom add-commutative (= (+ ?a ?b) (+ ?b ?a))
:evidence (evidence "Counting Observations"
:quotes ("The order of combining does not matter")
:explanation "Commutativity: a + b = b + a"))
(axiom mul-zero (= (* ?n zero) zero)
:evidence (evidence "Counting Observations"
:quotes ("We decided to mark an empty basket as \"zero\"")
:explanation "Multiplication by zero: n * 0 = 0"))
(axiom mul-succ (= (* ?n (succ ?m)) (+ (* ?n ?m) ?n))
:evidence (evidence "Counting Observations"
:quotes ("Multiplication is a shortcut for combining equal groups")
:explanation "Multiplication step: n * S(m) = n*m + n"))
; --- Variadic axioms via ?... splats ---
; These enable working with arbitrary numbers of piles at once,
; instead of nesting binary operations by hand.
; sum-all: combine any number of piles
; Base: a single pile is itself
(defterm sum-all :origin "variadic sum")
(axiom sum-all-base (= (sum-all ?x) ?x)
:evidence (evidence "Counting Observations"
:quotes ("Combining 🍎🍎🍎 apples with 🍎🍎 apples always gives 🍎🍎🍎🍎🍎 apples")
:explanation "A single pile needs no combining"))
; Step: peel off first pile, add to sum of remaining
(axiom sum-all-step (= (sum-all ?x ?y ?...rest) (+ ?x (sum-all ?y ?...rest)))
:evidence (evidence "Counting Observations"
:quotes ("Combining 🍎🍎🍎 apples with 🍎🍎 apples always gives 🍎🍎🍎🍎🍎 apples"
"The order of combining does not matter")
:explanation "Combine first pile with the sum of the rest"))
; count-gt: count how many piles exceed a threshold
; Base: single pile — is it greater?
(defterm count-gt :origin "variadic count")
(axiom count-gt-base (= (count-gt ?t ?x) (+ (if (> ?x ?t) 1 0) 0))
:evidence (evidence "Counting Observations"
:quotes ("If basket A has 🍎🍎🍎🍎🍎 and basket B has 🍎🍎🍎, then basket A has more")
:explanation "Check one pile against the threshold"))
; Step: check first, add to count of remaining
(axiom count-gt-step
(= (count-gt ?t ?x ?y ?...rest)
(+ (if (> ?x ?t) 1 0) (count-gt ?t ?y ?...rest)))
:evidence (evidence "Counting Observations"
:quotes ("If basket A has 🍎🍎🍎🍎🍎 and basket B has 🍎🍎🍎, then basket A has more"
"Combining 🍎🍎🍎 apples with 🍎🍎 apples always gives 🍎🍎🍎🍎🍎 apples")
:explanation "Check first pile, count the rest"))
; all-gt: are ALL piles above a threshold?
; Base: single pile
(defterm all-gt :origin "variadic check")
(axiom all-gt-base (= (all-gt ?t ?x) (> ?x ?t))
:evidence (evidence "Counting Observations"
:quotes ("If basket A has 🍎🍎🍎🍎🍎 and basket B has 🍎🍎🍎, then basket A has more")
:explanation "Check one pile against the threshold"))
; Step: all must pass
(axiom all-gt-step
(= (all-gt ?t ?x ?y ?...rest)
(and (> ?x ?t) (all-gt ?t ?y ?...rest)))
:evidence (evidence "Counting Observations"
:quotes ("If basket A has 🍎🍎🍎🍎🍎 and basket B has 🍎🍎🍎, then basket A has more")
:explanation "First pile must pass, and all remaining must too"))
; Morning harvest (same as apples_pltg)
(defterm eve-morning (succ (succ (succ zero)))
:evidence (evidence "Eden Inventory"
:quotes ("Eve picked 🍎🍎🍎 apples from the east grove")
:explanation "Eve's morning count: SSS0"))
(defterm adam-morning (succ (succ (succ (succ (succ zero)))))
:evidence (evidence "Eden Inventory"
:quotes ("Adam picked 🍎🍎🍎🍎🍎 apples from the west grove")
:explanation "Adam's morning count: SSSSS0"))
; Phase 1: Primitive symbols (same as apples_pltg)
(defterm zero
:evidence (evidence "Counting Observations"
:quotes ("We decided to mark an empty basket as \"zero\"")
:explanation "Zero: the label for an empty collection"))
(defterm succ
:evidence (evidence "Counting Observations"
:quotes ("every pile is reached by adding one more apple to the previous pile")
:explanation "Successor: produces the next pile"))
(defterm =
:evidence (evidence "Counting Observations"
:quotes ("If both baskets have 🍎🍎🍎🍎 apples, after swapping they still each have 🍎🍎🍎🍎")
:explanation "Equality: two piles that look the same"))
(defterm +
:evidence (evidence "Counting Observations"
:quotes ("Combining 🍎🍎🍎 apples with 🍎🍎 apples always gives 🍎🍎🍎🍎🍎 apples")
:explanation "Addition: combining two collections"))
(defterm -
:evidence (evidence "Counting Observations"
:quotes ("The difference is found by removing apples from the larger pile until it matches the smaller")
:explanation "Subtraction: finding the difference"))
(defterm >
:evidence (evidence "Counting Observations"
:quotes ("If basket A has 🍎🍎🍎🍎🍎 and basket B has 🍎🍎🍎, then basket A has more")
:explanation "Greater-than: heavier basket has more"))
(defterm *
:evidence (evidence "Counting Observations"
:quotes ("Multiplication is a shortcut for combining equal groups")
:explanation "Multiplication: repeated addition"))
(defterm and
:evidence (evidence "Counting Observations"
:quotes ("If basket A has 🍎🍎🍎🍎🍎 and basket B has 🍎🍎🍎, then basket A has more")
:explanation "Conjunction: both conditions must hold at once"))