←back to thread

114 points lemper | 2 comments | | HN request time: 0.473s | source
1. Animats ◴[] No.41918210[source]
It's easier if you start from something closer to Peano arithmetic or Boyer-Moore theory. I used to do a lot with constructive Boyer-Moore theory and their theorem prover. It starts with

    (ZERO)
and numbers are

    (ADD1 (ZERO))
    (ADD1 (ADD1 (ZERO)))
etc. The prover really worked that way internally, as I found out when I input a theorem with numbers such as 65536 in it. I was working on proving some things about 16-bit machine arithmetic, and those big numbers pushed SRI International's DECSystem 2060 into thrashing.

Here's the prover building up basic number theory, one theorem at a time.[1] This took about 45 minutes in 1981 and takes under a second now.

Constructive set theory without the usual set axioms is messy, though. The problem is equality. Informally, two sets are equal if they contain the same elements. But in a strict constructive representation, the representations have to be equal, and representations have order. So sets have to be stored sorted, which means much fiddly detail around maintaining a valid representation.

What we needed, but didn't have back then, was a concept of "objects". That is, two objects can be considered equal if they cannot be distinguished via their exported functions. I was groping around in that area back then, and had an ill-conceived idea of "forgetting", where, after you created an object and proved theorems about it, you "forgot" its private functions. Boyer and Moore didn't like that idea, and I didn't pursue it further.

Fun times.

[1] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...

replies(1): >>41919391 #
2. anthk ◴[] No.41919391[source]
The Computational Beauty of Nature has a tiny Lisp implementing integers and aritmethics by hand too, by consing t's.