diff --git a/docs/notebooks/BigInts.ipynb b/docs/notebooks/BigInts.ipynb index a600c95..7633eb9 100644 --- a/docs/notebooks/BigInts.ipynb +++ b/docs/notebooks/BigInts.ipynb @@ -2,14 +2,16 @@ "cells": [ { "cell_type": "code", - "execution_count": 1, + "execution_count": 51, "id": "73967878", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", - "text": [] + "text": [ + "[0 3 1]" + ] } ], "source": [ @@ -19,14 +21,16 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 52, "id": "b34d58ef", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", - "text": [] + "text": [ + "[0 3 1]" + ] } ], "source": [ @@ -47,7 +51,7 @@ }, { "cell_type": "markdown", - "id": "956c8ee2", + "id": "3f77ce91", "metadata": {}, "source": [ "## Take Two\n", @@ -58,341 +62,23 @@ { "cell_type": "code", "execution_count": null, - "id": "afe33f94", + "id": "b2845a8d", "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "code", - "execution_count": null, - "id": "03a44beb", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "9947b864", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "e91b6e37", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "8e7d4379", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "211669e7", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "d7ee0e4a", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "c9f34050", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "9d5972c4", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "cd6dc2e4", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "0beeac21", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "ccc32d74", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "7d2c5b56", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "83cbf474", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "be9be8d9", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "4c7df3f0", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "88f27acd", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "960edfef", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "2b3cad6c", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "7c613941", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "991f0d25", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "c3221039", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "ff5ab28c", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "58a46766", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "f488664c", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "5eefa527", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "d1f695de", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "22e5236c", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "5e069159", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "8e2fc444", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "025672cb", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "3359c82f", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "011563c0", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "f0e5eb9a", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "cb5a858d", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "936ef79c", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "e8a8bbe9", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "80672bab", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "aa635304", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "eba35315", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "14e8ca33", - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": 3, + "execution_count": 53, "id": "35476eac", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", - "text": [] + "text": [ + "[0 3 1]" + ] } ], "source": [ @@ -401,7 +87,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 54, "id": "02a48806", "metadata": {}, "outputs": [ @@ -420,7 +106,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 55, "id": "1d276daf", "metadata": {}, "outputs": [ @@ -440,7 +126,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 56, "id": "2454e662", "metadata": {}, "outputs": [ @@ -469,7 +155,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 57, "id": "8a60b54b", "metadata": {}, "outputs": [ @@ -509,7 +195,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 58, "id": "3fc98ccd", "metadata": {}, "outputs": [ @@ -529,7 +215,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 59, "id": "b838c4cb", "metadata": {}, "outputs": [ @@ -555,7 +241,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 60, "id": "faaac9d6", "metadata": {}, "outputs": [ @@ -576,7 +262,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 61, "id": "2a613f36", "metadata": {}, "outputs": [ @@ -598,7 +284,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 62, "id": "e97b149d", "metadata": {}, "outputs": [ @@ -619,7 +305,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 63, "id": "de4fe588", "metadata": {}, "outputs": [ @@ -637,7 +323,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 64, "id": "67bb934b", "metadata": {}, "outputs": [ @@ -657,8 +343,8 @@ }, { "cell_type": "code", - "execution_count": 15, - "id": "e4c66f15", + "execution_count": 65, + "id": "3d7ef5a7", "metadata": {}, "outputs": [ { @@ -675,7 +361,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 66, "id": "b6f77ac6", "metadata": {}, "outputs": [ @@ -703,7 +389,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 67, "id": "246c2a58", "metadata": {}, "outputs": [ @@ -723,7 +409,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 68, "id": "5a72ce30", "metadata": {}, "outputs": [ @@ -741,7 +427,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 69, "id": "59514dcd", "metadata": {}, "outputs": [ @@ -761,7 +447,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 70, "id": "f3c19364", "metadata": {}, "outputs": [ @@ -779,62 +465,1176 @@ "-1234567890123456789012345678901234567890 to_bigint" ] }, + { + "cell_type": "code", + "execution_count": 71, + "id": "00daba0b", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [] + } + ], + "source": [ + "clear" + ] + }, { "cell_type": "markdown", - "id": "4dbd0f30", + "id": "8157b5e7", "metadata": {}, "source": [ - "## Addition of Like Signs\n", + "## Addition of Like Signs `add-digits`\n", + "\n", + "Let's figure out how to add two lists of digits (we will assume that the signs are the same.) We need to put an inital `false` value for a carry flag, and then there's a `genrec`.\n", + "\n", + " initial-carry ≡ false rollup\n", + " add-digits' ≡ [P] [THEN] [R0] [R1] genrec\n", + " \n", + " add-digits ≡ initial-carry add-digits'" + ] + }, + { + "cell_type": "markdown", + "id": "fc9b97e4", + "metadata": {}, + "source": [ + "### The predicate\n", "\n", "I think we're going to want a recursive function (duh!?) but it's not quite a standard *hylomorphism* for (at least) two reasons:\n", "\n", "- We're tearing down two lists simultaneously.\n", "- They might not be the same length.\n", "\n", - "The base case would be two empty lists. In that case the result is determined by the `carry` bit, (Should zero be represented by the empty list `[]`, by `[0]`, or by both?) zero or one.\n", - "\n" + "There are two base cases: two empty lists or one empty list, the recursive branch is taken only if both lists at non-empty.\n", + "\n", + " bool [a ...] [b ...] P\n", + "\n", + "The first thing to do is convert them to Booleans:" ] }, { "cell_type": "code", - "execution_count": 21, - "id": "dd25bb96", + "execution_count": 72, + "id": "77eea97f", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "false" + "[[true true] [true false] [false true] [false false]]" ] } ], "source": [ "clear\n", - "\n", - "[] bool" + "[\n", + "[[a] [b]]\n", + "[[a] []]\n", + "[[] [b]]\n", + "[[] []]\n", + "]\n", + "[[[bool] ii] infra] \n", + "map" ] }, { "cell_type": "code", - "execution_count": 22, - "id": "c9bdd641", + "execution_count": 73, + "id": "b3d917b2", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "true" + "[[false] [true] [true] [true]]" + ] + } + ], + "source": [ + "clear\n", + "[\n", + "[[a] [b]]\n", + "[[a] []]\n", + "[[] [b]]\n", + "[[] []]\n", + "]\n", + "[[[bool] ii & not] infra] \n", + "map" + ] + }, + { + "cell_type": "markdown", + "id": "c37e6dc8", + "metadata": {}, + "source": [ + " P == [bool] ii & not" + ] + }, + { + "cell_type": "markdown", + "id": "2f69bbd1", + "metadata": {}, + "source": [ + "### The base cases\n", + "We have to decide between three cases, but because addition we can lump together the first two cases:\n", + "\n", + " bool [] [b ...] THEN\n", + " bool [a ...] [] THEN\n", + " bool [] [] THEN\n", + "\n", + " THEN ≡ [P'] [THEN'] [ELSE] ifte" + ] + }, + { + "cell_type": "code", + "execution_count": 74, + "id": "4a36d545", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[[true] [true] [false]]" + ] + } + ], + "source": [ + "clear\n", + "[\n", + "[[a] []]\n", + "[[] [b]]\n", + "[[] []]\n", + "]\n", + "[[[bool] ii |] infra] \n", + "map" + ] + }, + { + "cell_type": "markdown", + "id": "518f5c0d", + "metadata": {}, + "source": [ + " P' ≡ [bool] ii |\n", + "\n", + "So `THEN'` deals with one number (list of digits) being longer than the other, while the `ELSE` branch deals with the case of both lists being empty." + ] + }, + { + "cell_type": "markdown", + "id": "87db88e8", + "metadata": {}, + "source": [ + "#### One list empty\n", + "In the cases where one of the two lists (but not both) is empty:\n", + "\n", + " carry [a ...] [] THEN'\n", + " carry [] [b ...] THEN'\n", + "\n", + "We first get rid of the empty list:\n", + "\n", + " ditch-empty-list ≡ [bool] [popd] [pop] ifte" + ] + }, + { + "cell_type": "code", + "execution_count": 75, + "id": "3af0bfc7", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [] + } + ], + "source": [ + "clear\n", + "[ditch-empty-list [bool] [popd] [pop] ifte] inscribe" + ] + }, + { + "cell_type": "code", + "execution_count": 76, + "id": "85030079", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[1]" + ] + } + ], + "source": [ + "[1][] ditch-empty-list" + ] + }, + { + "cell_type": "code", + "execution_count": 77, + "id": "e4aafcaa", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[1]" + ] + } + ], + "source": [ + "clear\n", + "[][1] ditch-empty-list" + ] + }, + { + "cell_type": "markdown", + "id": "76a60ef3", + "metadata": {}, + "source": [ + " THEN' ≡ ditch-empty-list THEN''\n", + "\n", + "Now we have:\n", + "\n", + " carry [n ...] THEN''\n", + "\n", + "This is `add-carry-to-digits` that kicked my ass earlier today. Like I mentioned above, I think it was because I put it in the recursive branch! D'oh!" + ] + }, + { + "cell_type": "markdown", + "id": "b84cccef", + "metadata": {}, + "source": [ + "#### But first `add-with-carry`\n", + "We will want some function `F` that accepts a bool and two ints and leaves behind a new int and a new Boolean carry flag:\n", + "\n", + " carry0 a b F\n", + " --------------------------\n", + " (a+b+carry0) carry\n", + "\n", + "(I find it interesting that this function accepts the carry from below the int args but returns it above the result. Hmm...)" + ] + }, + { + "cell_type": "code", + "execution_count": 78, + "id": "3333e900", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "0 1" ] } ], "source": [ "clear\n", "\n", - "[] [] [bool not] ii &" + "[bool_to_int [0] [1] branch] inscribe\n", + "\n", + "false bool_to_int\n", + "true bool_to_int" ] }, + { + "cell_type": "code", + "execution_count": 79, + "id": "22a7c867", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "3" + ] + } + ], + "source": [ + "clear\n", + "\n", + "false 1 2 [bool_to_int] dipd + +" + ] + }, + { + "cell_type": "code", + "execution_count": 80, + "id": "75713ea2", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "4" + ] + } + ], + "source": [ + "clear\n", + "\n", + "true 1 2 [bool_to_int] dipd + +" + ] + }, + { + "cell_type": "markdown", + "id": "a9417aac", + "metadata": {}, + "source": [ + "So the first part of `F` is `[bool_to_int] dipd + +` to get the total, then we need to" + ] + }, + { + "cell_type": "code", + "execution_count": 81, + "id": "b4f1000f", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "4 false" + ] + } + ], + "source": [ + "clear\n", + "\n", + "4 base [mod] [>=] clop" + ] + }, + { + "cell_type": "code", + "execution_count": 82, + "id": "ffbdf325", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "100 true" + ] + } + ], + "source": [ + "clear\n", + "\n", + "base 100 +\n", + "\n", + "base [mod] [>=] clop" + ] + }, + { + "cell_type": "markdown", + "id": "f09689c3", + "metadata": {}, + "source": [ + "Put it all together and we have:\n", + "\n", + " _add-with-carry0 ≡ [bool_to_int] dipd + +\n", + " _add-with-carry1 ≡ base [mod] [>=] clop\n", + "\n", + " add-with-carry ≡ _add-with-carry0 _add-with-carry1\n" + ] + }, + { + "cell_type": "code", + "execution_count": 83, + "id": "b8161efb", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [] + } + ], + "source": [ + "clear\n", + "[_add-with-carry0 [bool_to_int] dipd + +] inscribe\n", + "[_add-with-carry1 base [mod] [>=] clop] inscribe\n", + "[add-with-carry _add-with-carry0 _add-with-carry1] inscribe" + ] + }, + { + "cell_type": "code", + "execution_count": 84, + "id": "0f082af7", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "100 true" + ] + } + ], + "source": [ + "clear\n", + "\n", + "false base 100 add-with-carry" + ] + }, + { + "cell_type": "code", + "execution_count": 85, + "id": "a0d656bf", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "101 true" + ] + } + ], + "source": [ + "clear\n", + "\n", + "true base 100 add-with-carry" + ] + }, + { + "cell_type": "code", + "execution_count": 86, + "id": "fb7065be", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "102 false" + ] + } + ], + "source": [ + "clear\n", + "\n", + "false 2 100 add-with-carry" + ] + }, + { + "cell_type": "code", + "execution_count": 87, + "id": "9b91363f", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "103 false" + ] + } + ], + "source": [ + "clear\n", + "\n", + "true 2 100 add-with-carry" + ] + }, + { + "cell_type": "code", + "execution_count": 89, + "id": "5596f574", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [] + } + ], + "source": [ + "clear" + ] + }, + { + "cell_type": "markdown", + "id": "861e6896", + "metadata": {}, + "source": [ + "### Now back to `add-carry-to-digits`\n", + "\n", + "This should be a very simple recursive function.\n", + "\n", + " add-carry-to-digits ≡ [_actd_P] [_actd_THEN] [_actd_R0] [_actd_R1] genrec\n", + "\n", + " carry [n ...] add-carry-to-digits\n", + " carry [n ...] [_actd_P] [_actd_THEN] [_actd_R0] [_actd_R1] genrec\n", + "\n", + "The predicate is the carry flag itself inverted, but when we recur we need to check if the list is non-empty because it will eventually be empty or the carry flag will be false:\n", + "\n", + " _actd_P ≡ pop not\n", + "\n", + "The base case simply discards the carry flag:\n", + "\n", + " _actd_THEN ≡ popd" + ] + }, + { + "cell_type": "markdown", + "id": "26ba75fb", + "metadata": {}, + "source": [ + "That leaves the recursive branch:\n", + "\n", + " true [n ...] R0 [add-carry-to-digits] R1\n", + "\n", + "-or-\n", + "\n", + " true [] R0 [add-carry-to-digits] R1" + ] + }, + { + "cell_type": "markdown", + "id": "4d66332b", + "metadata": {}, + "source": [ + "We know that the Boolean value is `true`. We also know that the list will be non-empty, but only on the first iteration of the `genrec`. It may be that the list is empty on a later iteration.\n", + "\n", + "The `R0` function should check the list.\n", + "\n", + " _actd_R0 ≡ [bool] [_actd_R0.then] [_actd_R0.else] ifte" + ] + }, + { + "cell_type": "markdown", + "id": "4ed0fd33", + "metadata": {}, + "source": [ + "If it's empty...\n", + "\n", + " true [] R0.else [add-carry-to-digits] R1\n", + " ----------------------------------------------\n", + " false [1] [add-carry-to-digits] R1\n", + "\n", + " R0.else ≡ 1 swons popd false swap" + ] + }, + { + "cell_type": "markdown", + "id": "e82f8749", + "metadata": {}, + "source": [ + "If it's not empty...\n", + "\n", + " true [a ...] R0.then [add-carry-to-digits] R1\n", + " -------------------------------------------------------------\n", + " true 0 a add-with-carry [...1] [add-carry-to-digits] R1\n", + " -------------------------------------------------------------\n", + " (a+1) carry [...1] [add-carry-to-digits] R1" + ] + }, + { + "cell_type": "markdown", + "id": "07f1bc97", + "metadata": {}, + "source": [ + "Ah ha!? How to get that `(a+1)` back into the list!?\n", + "\n", + "If it's empty...\n", + "\n", + " true [] R0.else [add-carry-to-digits] R1\n", + " ------------------------------------------------\n", + " 1 false [] [add-carry-to-digits] i cons\n", + "\n", + "and\n", + "\n", + " true [a ...] R0.then [add-carry-to-digits] i cons\n", + " -------------------------------------------------------------\n", + " true 0 a add-with-carry [...1] [add-carry-to-digits] i cons\n", + " -------------------------------------------------------------\n", + " (a+1) carry [...1] [add-carry-to-digits] i cons" + ] + }, + { + "cell_type": "markdown", + "id": "9bfc7127", + "metadata": {}, + "source": [ + "There we go.\n", + "\n", + " _actd_R0.else ≡ popd 1 false rolldown\n", + "\n", + " _actd_R0.then ≡ 0 swap uncons [add-with-carry] dip\n", + "\n", + " _actd_R1 ≡ i cons" + ] + }, + { + "cell_type": "code", + "execution_count": 90, + "id": "6bd105a9", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [] + } + ], + "source": [ + "[add-carry-to-digits [_actd_P] [_actd_THEN] [_actd_R0] [_actd_R1] genrec] inscribe\n", + "[_actd_P pop not] inscribe\n", + "[_actd_THEN popd] inscribe\n", + "[_actd_R0 [bool] [_actd_R0.then] [_actd_R0.else] ifte] inscribe\n", + "[_actd_R0.else popd 1 false rolldown] inscribe\n", + "[_actd_R0.then 0 swap uncons [add-with-carry] dip] inscribe\n", + "[_actd_R1 i cons] inscribe" + ] + }, + { + "cell_type": "code", + "execution_count": 91, + "id": "39244b26", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[3 2 1]" + ] + } + ], + "source": [ + "clear\n", + "\n", + "false [3 2 1] add-carry-to-digits" + ] + }, + { + "cell_type": "code", + "execution_count": 92, + "id": "0a921fd7", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[1]" + ] + } + ], + "source": [ + "clear\n", + "\n", + "true [] add-carry-to-digits" + ] + }, + { + "cell_type": "code", + "execution_count": 93, + "id": "94359309", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[4 2 1]" + ] + } + ], + "source": [ + "clear\n", + "\n", + "true [3 2 1] add-carry-to-digits" + ] + }, + { + "cell_type": "code", + "execution_count": 94, + "id": "d5d4de95", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "true [2147483647 2 1]" + ] + } + ], + "source": [ + "clear\n", + "\n", + "true base -- [2 1] cons " + ] + }, + { + "cell_type": "code", + "execution_count": 95, + "id": "a34b4771", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[0 3 1]" + ] + } + ], + "source": [ + "add-carry-to-digits" + ] + }, + { + "cell_type": "markdown", + "id": "181cdfd4", + "metadata": {}, + "source": [ + "So that handles the cases where one of the two lists (but not both) is empty.\n", + "\n", + "#### Both lists empty\n", + "If both lists are empty we discard one list and check the carry to determine our result as decribed above:\n", + "\n", + " ELSE ≡ pop swap [] [1 swons] branch" + ] + }, + { + "cell_type": "code", + "execution_count": 96, + "id": "5e5ddf74", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[1]" + ] + } + ], + "source": [ + "clear\n", + "\n", + "true [] [] pop swap [] [1 swons] branch" + ] + }, + { + "cell_type": "code", + "execution_count": 97, + "id": "c57d1fb2", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[]" + ] + } + ], + "source": [ + "clear\n", + "\n", + "false [] [] pop swap [] [1 swons] branch" + ] + }, + { + "cell_type": "code", + "execution_count": 98, + "id": "59b1338c", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [] + } + ], + "source": [ + "clear" + ] + }, + { + "cell_type": "markdown", + "id": "c4454f63", + "metadata": {}, + "source": [ + "The story so far...\n", + "\n", + " add-digits ≡ initial-carry add-digits'\n", + " \n", + " add-digits' ≡ [P] [THEN] [R0] [R1] genrec\n", + "\n", + " initial-carry ≡ false rollup\n", + "\n", + " P ≡ [bool] ii & not\n", + "\n", + " THEN ≡ [P'] [THEN'] [ELSE] ifte\n", + "\n", + " P' ≡ [bool] ii |\n", + "\n", + " THEN' ≡ ditch-empty-list add-carry-to-digits\n", + "\n", + " ELSE ≡ pop swap [] [1 swons] branch\n", + "\n", + "We just need to knock out those recursive functions `R0` and `R1` and we're done." + ] + }, + { + "cell_type": "markdown", + "id": "54632eea", + "metadata": {}, + "source": [ + "### And recur...\n", + "\n", + " bool [a ...] [b ...] R0 [add-digits'] R1" + ] + }, + { + "cell_type": "markdown", + "id": "995bd8d3", + "metadata": {}, + "source": [ + "First we will want to `uncons` the digits" + ] + }, + { + "cell_type": "code", + "execution_count": 99, + "id": "02c19af8", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "false 1 4 [2 3] [5 6]" + ] + } + ], + "source": [ + "clear\n", + "\n", + "false [1 2 3] [4 5 6] [uncons] ii swapd" + ] + }, + { + "cell_type": "markdown", + "id": "9557420b", + "metadata": {}, + "source": [ + "#### `uncons-two`\n", + "We could call this `uncons-two`:" + ] + }, + { + "cell_type": "code", + "execution_count": 100, + "id": "5d671aa4", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "1 4 [2 3] [5 6]" + ] + } + ], + "source": [ + "clear\n", + "\n", + "[uncons-two [uncons] ii swapd] inscribe\n", + "\n", + "[1 2 3] [4 5 6] uncons-two" + ] + }, + { + "cell_type": "code", + "execution_count": 102, + "id": "80eab7d7", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [] + } + ], + "source": [ + "clear" + ] + }, + { + "cell_type": "markdown", + "id": "a47c67cf", + "metadata": {}, + "source": [ + " bool a b [...] [...] R0' [add-digits'] R1\n", + "\n", + "It's at this point that we'll want to employ the `add-with-carry` function:\n", + "\n", + " bool a b [...] [...] [add-with-carry] dipd R0'' [add-digits'] R1\n", + "\n", + " bool a b add-with-carry [...] [...] R0'' [add-digits'] R1\n", + "\n", + " (a+b) bool [...] [...] R0'' [add-digits'] R1\n", + "\n", + "If we postulate a `cons` in our `R1` function...\n", + "\n", + " (a+b) bool [...] [...] R0'' [add-digits'] i cons\n", + "\n", + "Then it seems like we're done? `R0''` is nothing?\n", + "\n", + " R0 ≡ uncons-two [add-with-carry] dipd\n", + " \n", + " R1 ≡ i cons\n" + ] + }, + { + "cell_type": "code", + "execution_count": 103, + "id": "a16c95cf", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [] + } + ], + "source": [ + "[add-digits initial-carry add-digits'] inscribe\n", + "[add-digits' [P] [THEN] [R0] [R1] genrec] inscribe\n", + "[initial-carry false rollup] inscribe\n", + "[P [bool] ii & not] inscribe\n", + "[THEN [P'] [THEN'] [ELSE] ifte] inscribe\n", + "[P' [bool] ii |] inscribe\n", + "[THEN' ditch-empty-list add-carry-to-digits] inscribe\n", + "[ELSE pop swap [] [1 swons] branch] inscribe\n", + "[R0 uncons-two [add-with-carry] dipd] inscribe\n", + "[R1 i cons] inscribe\n" + ] + }, + { + "cell_type": "code", + "execution_count": 104, + "id": "66176a8f", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[3 2 1] [1 1 1]" + ] + } + ], + "source": [ + "[3 2 1] [1 1 1]" + ] + }, + { + "cell_type": "code", + "execution_count": 105, + "id": "e0272194", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[4 3 2]" + ] + } + ], + "source": [ + "add-digits" + ] + }, + { + "cell_type": "code", + "execution_count": 106, + "id": "bec3b32d", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[4 3 2] [2147483647]" + ] + } + ], + "source": [ + "base -- unit" + ] + }, + { + "cell_type": "code", + "execution_count": 107, + "id": "6d8b0054", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[3 4 2]" + ] + } + ], + "source": [ + "add-digits" + ] + }, + { + "cell_type": "code", + "execution_count": 108, + "id": "c842f875", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[3 4 2] [2147483647 2147483647 2147483647]" + ] + } + ], + "source": [ + "base -- dup dup unit ccons" + ] + }, + { + "cell_type": "code", + "execution_count": 109, + "id": "80a240b0", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[2 4 2 1]" + ] + } + ], + "source": [ + "add-digits" + ] + }, + { + "cell_type": "markdown", + "id": "558e0a6d", + "metadata": {}, + "source": [ + "243 + 999 = " + ] + }, + { + "cell_type": "code", + "execution_count": 110, + "id": "31aa6611", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "1242" + ] + } + ], + "source": [ + "clear 243 999 +" + ] + }, + { + "cell_type": "markdown", + "id": "db2de9c5", + "metadata": {}, + "source": [ + "Bitchin'" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "a46d9942", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "4fe39366", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "ef9db281", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "834ee60c", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "20a2809e", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "b74e8780", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "b2765992", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "c96c51a5", + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "markdown", "id": "50665e75", @@ -942,87 +1742,6 @@ "[1][1]_add_p" ] }, - { - "cell_type": "markdown", - "id": "abe20e0b", - "metadata": {}, - "source": [ - "### Base Case\n", - "In the base case we discard one list and check the carry to determine our result as decribed above:" - ] - }, - { - "cell_type": "code", - "execution_count": 127, - "id": "5e5ddf74", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[1]" - ] - } - ], - "source": [ - "clear\n", - "\n", - "true [] [] pop swap [] [1 swons] branch" - ] - }, - { - "cell_type": "code", - "execution_count": 128, - "id": "c57d1fb2", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[]" - ] - } - ], - "source": [ - "clear\n", - "\n", - "false [] [] pop swap [] [1 swons] branch" - ] - }, - { - "cell_type": "code", - "execution_count": 129, - "id": "59b1338c", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [] - } - ], - "source": [ - "clear" - ] - }, - { - "cell_type": "code", - "execution_count": 31, - "id": "ed38fdb1", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [] - } - ], - "source": [ - "[_add_then pop swap [] [1 swons] branch] inscribe" - ] - }, { "cell_type": "markdown", "id": "978b5cac", @@ -1160,386 +1879,6 @@ "[_add_rec_pred [bool] ii &] inscribe" ] }, - { - "cell_type": "markdown", - "id": "2adf3f59", - "metadata": {}, - "source": [ - "#### `true` branch\n", - "Let's square away the `true` branch first.\n", - "\n", - " carry [a ...] [b ...] ... [add_digits] ...\n", - "\n", - "First we will want to `uncons` the digits" - ] - }, - { - "cell_type": "code", - "execution_count": 95, - "id": "1e53236f", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "false 1 4 [2 3] [5 6]" - ] - } - ], - "source": [ - "clear\n", - "\n", - "false [1 2 3] [4 5 6] [uncons] ii swapd" - ] - }, - { - "cell_type": "markdown", - "id": "8d66b26b", - "metadata": {}, - "source": [ - "#### add-with-carry\n", - "So now we want some function `F` to `dipd` below the list tails that accepts a bool and two ints and leaves behind a new int and a new Boolean carry flag:\n", - "\n", - " carry0 a b F\n", - " --------------------------\n", - " (a+b+carry0) carry\n", - "\n", - "(I find it interesting that this function accepts the carry from below the int args but returns it above the result. Hmm...)" - ] - }, - { - "cell_type": "code", - "execution_count": 96, - "id": "2f70ca25", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "0 1" - ] - } - ], - "source": [ - "clear\n", - "\n", - "[bool_to_int [0] [1] branch] inscribe\n", - "\n", - "false bool_to_int\n", - "true bool_to_int" - ] - }, - { - "cell_type": "code", - "execution_count": 97, - "id": "c19916c5", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "3" - ] - } - ], - "source": [ - "clear\n", - "\n", - "false 1 2 [bool_to_int] dipd + +" - ] - }, - { - "cell_type": "code", - "execution_count": 98, - "id": "ead4cc5e", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "4" - ] - } - ], - "source": [ - "clear\n", - "\n", - "true 1 2 [bool_to_int] dipd + +" - ] - }, - { - "cell_type": "markdown", - "id": "ddb201ca", - "metadata": {}, - "source": [ - "So the first part of `F` is `[bool_to_int] dipd + +` to get the total, then we need to" - ] - }, - { - "cell_type": "code", - "execution_count": 99, - "id": "129997e0", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "4" - ] - } - ], - "source": [ - "base mod" - ] - }, - { - "cell_type": "code", - "execution_count": 100, - "id": "22209a15", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "false" - ] - } - ], - "source": [ - "base >=" - ] - }, - { - "cell_type": "code", - "execution_count": 101, - "id": "57649cf3", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "4 false" - ] - } - ], - "source": [ - "clear\n", - "\n", - "4 base [mod] [>=] clop" - ] - }, - { - "cell_type": "code", - "execution_count": 102, - "id": "3c2e42be", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "100 true" - ] - } - ], - "source": [ - "clear\n", - "\n", - "base 100 +\n", - "\n", - "base [mod] [>=] clop" - ] - }, - { - "cell_type": "markdown", - "id": "893a39c4", - "metadata": {}, - "source": [ - "\n", - " F == [bool_to_int] dipd + + base [mod] [>=] clop\n" - ] - }, - { - "cell_type": "code", - "execution_count": 103, - "id": "257d757c", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [] - } - ], - "source": [ - "clear\n", - "[_add-with-carry0 [bool_to_int] dipd + +] inscribe\n", - "[_add-with-carry1 base [mod] [>=] clop] inscribe\n", - "[add-with-carry _add-with-carry0 _add-with-carry1] inscribe" - ] - }, - { - "cell_type": "code", - "execution_count": 104, - "id": "1d50a1c6", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "100 true" - ] - } - ], - "source": [ - "clear\n", - "\n", - "false base 100 add-with-carry" - ] - }, - { - "cell_type": "code", - "execution_count": 105, - "id": "b93ae376", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "101 true" - ] - } - ], - "source": [ - "clear\n", - "\n", - "true base 100 add-with-carry" - ] - }, - { - "cell_type": "code", - "execution_count": 106, - "id": "4f86c2c7", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "102 false" - ] - } - ], - "source": [ - "clear\n", - "\n", - "false 2 100 add-with-carry" - ] - }, - { - "cell_type": "code", - "execution_count": 107, - "id": "68a8a9c2", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "103 false" - ] - } - ], - "source": [ - "clear\n", - "\n", - "true 2 100 add-with-carry" - ] - }, - { - "cell_type": "markdown", - "id": "e9a512f0", - "metadata": {}, - "source": [ - "Going back to our `true` branch we have:" - ] - }, - { - "cell_type": "code", - "execution_count": 108, - "id": "74873f5b", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "false 1 4 [2 3] [5 6]" - ] - } - ], - "source": [ - "clear\n", - "\n", - "false [1 2 3] [4 5 6] [uncons] ii swapd" - ] - }, - { - "cell_type": "markdown", - "id": "5520db54", - "metadata": {}, - "source": [ - "#### `uncons-two`\n", - "We could call this `uncons-two`:" - ] - }, - { - "cell_type": "code", - "execution_count": 116, - "id": "e7176ea9", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "1 4 [2 3] [5 6]" - ] - } - ], - "source": [ - "clear\n", - "\n", - "[uncons-two [uncons] ii swapd] inscribe\n", - "\n", - "[1 2 3] [4 5 6] uncons-two" - ] - }, - { - "cell_type": "code", - "execution_count": 117, - "id": "64b575f7", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [] - } - ], - "source": [ - "clear" - ] - }, { "cell_type": "markdown", "id": "9445eb3c", @@ -1651,75 +1990,6 @@ "clear" ] }, - { - "cell_type": "markdown", - "id": "85a49679", - "metadata": {}, - "source": [ - "#### `false` branch\n", - "And now we deal with the cases where one of the two lists (but not both) is empty:\n", - "\n", - " carry [a ...] [] ELSE\n", - " carry [] [b ...] ELSE\n", - "\n", - "We get rid of the empty list:\n", - "\n", - "[bool] [popd] [pop] ifte" - ] - }, - { - "cell_type": "code", - "execution_count": 113, - "id": "affd02fb", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [] - } - ], - "source": [ - "[ditch-empty-list [bool] [popd] [pop] ifte] inscribe" - ] - }, - { - "cell_type": "code", - "execution_count": 114, - "id": "5cc19cea", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[1]" - ] - } - ], - "source": [ - "[1][] ditch-empty-list" - ] - }, - { - "cell_type": "code", - "execution_count": 115, - "id": "12d72692", - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[1]" - ] - } - ], - "source": [ - "clear\n", - "[][1] ditch-empty-list" - ] - }, { "cell_type": "markdown", "id": "aa76c2fc",