4 ms·
By the way, another analogy: I recently wrote a microKanren in F#. I taught this microKanren arithmetic with the Peano naturals; it knew how to count, and it kn
by Smaug123 5y ago
By the way, another analogy: I recently wrote a microKanren in F#. I taught this microKanren arithmetic with the Peano naturals; it knew how to count, and it knew what 37 was, but the encoding is very inefficient and it was slow to count.
Then (https://github.com/Smaug123/FicroKanSharp/blob/912d9cd5d2e65bec2b685a8b722fbec5e50a9d8b/FicroKanSharp.Test/TypedArithmetic.fs#L9 https://github.com/Smaug123/FicroKanSharp/blob/912d9cd5d2e65...) I added the ability for the user to supply custom unification rules, and created a new representation of the naturals: "a natural is an F# integer, or a term representing the successor of a natural". I supplied custom unification rules so that e.g. 1 would unify with Succ(0).
With this done, natural numbers were in some sense represented natively in the microKanren. Rather than it having to think about how to compute with them, the F# runtime would do many computations without those computations having to live in microKanren "emulated" space.
The analogy is that the microKanren now experiences natural numbers (not that I believe the microKanren was conscious, nor that my world-model is anything like microKanren - it's just an analogy). It has a new, native representation that is entirely "unconscious"ly available to it. Mary steps out of the room, and instead of shuffling around Succ(Succ(Zero)), she now has the immediate "intuitive" representation that is the F# integer 2. No new knowledge; a new representation.