Lambda Calc, Peano Axioms, & Recreating Maths

I tried to make all math from just 3 functions! Here is the script:
Math-bootstrap script pic

(The "primitive" functions are S(x), S⁻¹(x), and aₙ.)

For lambda calc:

Open in a new tab

Good start!

If it were me, I would have called that last one f n.

The way mathematicians typically do this is to restrict attention to the nonnegative integers (natural numbers), in which case you don't need the predecessor function. See Peano axioms, which, like all the math articles in Wikipedia, is written for mathematicians rather than for regular people, but which probably has more readable sources in its references.

Computer scientists, on the other hand, do it using Church numerals, based on lambda calculus, in which the only primitives are λ (Snap!: untitled script pic (2)) and application (Snap!: untitled script pic (3)). To save you having to fight Wikipedia, here's a Snap! project on Church numerals:

Church.pdf (1.3 MB)

Thank you. I read and tried to follow that λ calc in Snap! pdf before. I'll look into the Peano Axioms. Restricting it to ℕ makes sense.

This might be probably is a dumb question, but is there any way to do subtraction under the rules of the Peano Axioms?

Yes, depending on which variant you use. Some versions include the axiom ∀x,y | (S(x) = S(y)) ➞ (x = y). In those versions there's a function S−1 defined on all x > 0. So you can use that to implement subtraction, but of course x−y is defined only if x≥y.

P.S. The only dumb question is "Is this going to be on the quiz?"

The new version: Math-bootstrap script pic

Thank you! What would you recommend for division? I'd guess I would just floor the result and provide mod.

I like to watch Ben Eater's building a computer on a breadboard series, and MAN does division seem complicated.


On another note, I just accidentally found a way to rearrange the palette.

I'm thinking about making my own datatype to represent numbers.

Here is my new version with it:
Math-bootstrap script pic

Right click and you should see unringify.

Thanks!

That'd work. Instead of doing real division and flooring the result, you should really do repeated subtraction, same as multiplication is repeated addition.

The other thing is to invent pairs (lists of length 2) and report the integer quotient and remainder.

Everything is complicated on real computers, because the simple algorithms are slow. :~)

That's cool, but it's cheating if you convert to Snap! numbers to do the actual work. You can do that to examine the results, for debugging, but it doesn't really count as inventing your own numbers unless they can support the doing of arithmetic in their own terms.

It looks kind of like Church numerals except that the function you repeat is always U instead of being an input to the number.

The only conversions are to see the answer and to make loops work.

I got the idea from church numerals.

"To make loops work" counts! That's most of the work you do. :~)

I don't want to be a cheater! I'll figure this out right away!

How would you implement division by repeated subtraction?

with variables n (10) and count (0) and factor (5) --
repeat until n=0: thisCoolProcedure(
change n by negative factor
if n > factor:
change count by 1
thisCoolProcedure
else:
set factor to factor/2
change count by 0.5
thisCoolProcedure
)
hey check out: count

EDIT: this probably wouldn't work because it only handles wholes and 0.5s

I'm restricting it to ℕ so it will work, though you do have dividing by 2 in the proc.

U is essentially the Successor Function.

I know. I guess I was wrong, it's just NUMBER that has U built in. So, yeah, that's basically Church numerals only with named functions (which matters once you want to do recursion).

I'll follow along with the lambda calc.


I'm stuck on plus.... here's my project

For a given number n, to add number q, call the successor of n q times.