sforman
/
Thun
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
Thun/docs/notebooks/BigInts.ipynb

3384 lines
68 KiB
Plaintext
Raw Blame History

{
"cells": [
{
"cell_type": "code",
"execution_count": 51,
"id": "73967878",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[0 3 1]"
]
}
],
"source": [
"[all true swap [&] step] inscribe\n",
"[any false swap [|] step] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 52,
"id": "b34d58ef",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[0 3 1]"
]
}
],
"source": [
"[base 2147483648] inscribe"
]
},
{
"cell_type": "markdown",
"id": "9749000b",
"metadata": {},
"source": [
"Model bigints as a pair of Boolean for the sign and a list of integers for the digits, to keep things simple let the bool be the first item on a list followed by zero or more int digits. The digits shall be confined to the range zero to `pow(2, 31) - 1`\n",
"\n",
"Another way to say that is that our numbers are in base `2147483648` and our \"nine\" is `2147483647` (`0b1111111111111111111111111111111`, 31 ones.)\n",
"\n",
"This lets us use (Oberon RISC) 32-bit signed ints to store our digits."
]
},
{
"cell_type": "markdown",
"id": "3f77ce91",
"metadata": {},
"source": [
"## Take Two\n",
"\n",
"This really got away from me the first time. I think the big mistake ai made was including the middle branch in the recursive branch.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "b2845a8d",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": 53,
"id": "35476eac",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[0 3 1]"
]
}
],
"source": [
"[valid_digit [0 >] [base <] &&] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 54,
"id": "02a48806",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"32 true 1232147483648 false"
]
}
],
"source": [
"clear\n",
"32 valid_digit 1232147483648 valid_digit"
]
},
{
"cell_type": "code",
"execution_count": 55,
"id": "1d276daf",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"true"
]
}
],
"source": [
"clear\n",
"[true 3 2 1]\n",
"rest [valid_digit] map all"
]
},
{
"cell_type": "code",
"execution_count": 56,
"id": "2454e662",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[true 3 2 1]"
]
}
],
"source": [
"clear\n",
"[true 3 2 1]"
]
},
{
"cell_type": "markdown",
"id": "bfed1f25",
"metadata": {},
"source": [
"Because we are working with Python Joy right now we can convert ints to bigints.\n",
"\n",
"To get the sign bool we can just use `!-` (\"not negative\")"
]
},
{
"cell_type": "code",
"execution_count": 57,
"id": "8a60b54b",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"true false"
]
}
],
"source": [
"clear\n",
"23 !- -23 !-"
]
},
{
"cell_type": "markdown",
"id": "73bfa634",
"metadata": {},
"source": [
"To get the list of digits...\n",
"\n",
"```\n",
" @staticmethod\n",
" def digitize(n):\n",
" if n < 0:\n",
" raise ValueError(f'Non-negative only: {n}')\n",
" while n:\n",
" n, digit = divmod(n, 2**31)\n",
" yield OberonInt(digit)\n",
"\n",
"```\n",
"\n",
" [0 >=] [base divmod swap] while"
]
},
{
"cell_type": "code",
"execution_count": 58,
"id": "3fc98ccd",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"1797196498 5748904729"
]
}
],
"source": [
"clear\n",
"\n",
"12345678901234567890 base divmod swap"
]
},
{
"cell_type": "code",
"execution_count": 59,
"id": "b838c4cb",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"1797196498 1453937433 2"
]
}
],
"source": [
"base divmod swap"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "4d9d926a",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": 60,
"id": "faaac9d6",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"1312754386 1501085485 57659106 105448366 58"
]
}
],
"source": [
"clear\n",
"\n",
"1234567890123456789012345678901234567890\n",
" [0 >] [base divmod swap] while pop"
]
},
{
"cell_type": "code",
"execution_count": 61,
"id": "2a613f36",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[58 105448366 57659106 1501085485 1312754386]"
]
}
],
"source": [
"clear\n",
"\n",
"[1234567890123456789012345678901234567890]\n",
" [ [0 >] [base divmod swap] while pop ]\n",
" infra"
]
},
{
"cell_type": "code",
"execution_count": 62,
"id": "e97b149d",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"1234567890123456789012345678901234567890 [0 <=] [pop []] [base divmod swap] [i cons]"
]
}
],
"source": [
"clear\n",
"\n",
"1234567890123456789012345678901234567890\n",
" [0 <=] [pop []] [base divmod swap] [i cons]"
]
},
{
"cell_type": "code",
"execution_count": 63,
"id": "de4fe588",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[1312754386 1501085485 57659106 105448366 58]"
]
}
],
"source": [
"genrec"
]
},
{
"cell_type": "code",
"execution_count": 64,
"id": "67bb934b",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[]"
]
}
],
"source": [
"clear\n",
"\n",
"0 [0 <=] [pop []] [base divmod swap] [i cons] genrec"
]
},
{
"cell_type": "code",
"execution_count": 65,
"id": "3d7ef5a7",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear\n",
"\n",
"[digitalize [0 <=] [pop []] [base divmod swap] [i cons] genrec] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 66,
"id": "b6f77ac6",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[1312754386 1501085485 57659106 105448366 58]"
]
}
],
"source": [
"clear\n",
"\n",
"1234567890123456789012345678901234567890 digitalize"
]
},
{
"cell_type": "markdown",
"id": "1bf8ba9e",
"metadata": {},
"source": [
"So `!-` for the sign and `abs digitalize` for the digits, followed by `cons`:"
]
},
{
"cell_type": "code",
"execution_count": 67,
"id": "246c2a58",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[true 1312754386 1501085485 57659106 105448366 58]"
]
}
],
"source": [
"clear\n",
"\n",
"1234567890123456789012345678901234567890 [!-] [abs digitalize] cleave cons"
]
},
{
"cell_type": "code",
"execution_count": 68,
"id": "5a72ce30",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[true 1312754386 1501085485 57659106 105448366 58]"
]
}
],
"source": [
"[to_bigint [!-] [abs digitalize] cleave cons] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 69,
"id": "59514dcd",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[true 1312754386 1501085485 57659106 105448366 58]"
]
}
],
"source": [
"clear\n",
"\n",
"1234567890123456789012345678901234567890 to_bigint"
]
},
{
"cell_type": "code",
"execution_count": 70,
"id": "f3c19364",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[false 1312754386 1501085485 57659106 105448366 58]"
]
}
],
"source": [
"clear\n",
"\n",
"-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": "8157b5e7",
"metadata": {},
"source": [
"## 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",
"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": 72,
"id": "77eea97f",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[[true true] [true false] [false true] [false false]]"
]
}
],
"source": [
"clear\n",
"[\n",
"[[a] [b]]\n",
"[[a] []]\n",
"[[] [b]]\n",
"[[] []]\n",
"]\n",
"[[[bool] ii] infra] \n",
"map"
]
},
{
"cell_type": "code",
"execution_count": 73,
"id": "b3d917b2",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[[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_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",
"metadata": {},
"source": [
"### Predicate\n",
"so the predicate for the whole thing would be"
]
},
{
"cell_type": "code",
"execution_count": 121,
"id": "187aa6ec",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear\n",
"\n",
"[_add_p [bool not] ii &] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 123,
"id": "ee3d2316",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"true"
]
}
],
"source": [
"clear\n",
"\n",
"[][]_add_p"
]
},
{
"cell_type": "code",
"execution_count": 124,
"id": "7e8c4942",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false"
]
}
],
"source": [
"clear\n",
"\n",
"[1][]_add_p"
]
},
{
"cell_type": "code",
"execution_count": 125,
"id": "8b41766c",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false"
]
}
],
"source": [
"clear\n",
"\n",
"[][1]_add_p"
]
},
{
"cell_type": "code",
"execution_count": 126,
"id": "1bacc617",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false"
]
}
],
"source": [
"clear\n",
"\n",
"[1][1]_add_p"
]
},
{
"cell_type": "markdown",
"id": "978b5cac",
"metadata": {},
"source": [
"### Recursive Branch\n",
"So (ignoring the source of the initial carry bit for now) we have:\n",
"\n",
" _add_p == [bool not] ii &\n",
" _add_then == pop swap [] [1 swons] branch\n",
"\n",
" add_digits == [_add_p] [_add_then] [R0] [R1] genrec\n",
"\n",
"What should the recursive branch do?\n",
"\n",
"It will be some `ifte` expression:\n",
"\n",
" R0 [add_digits] R1 == [P] [THEN] [ELSE] ifte\n",
"\n",
"Ideally, we can arrange to neatly bracket the `[add_digits]` quote, but otherwise we can build up the `ifte` quotes in the usual way with `cons` and `concat`."
]
},
{
"cell_type": "markdown",
"id": "7246fe3d",
"metadata": {},
"source": [
"#### Is One List Empty?\n",
"The context will be a Boolean carry bit and two lists, one of which (but not both!) may be empty.\n",
"\n",
" carry [a ...] [b ...] R0 [add_digits] R1\n",
"\n",
" carry [] [b ...] R0 [add_digits] R1\n",
"\n",
" carry [a ...] [] R0 [add_digits] R1\n",
"\n",
"So I think the first thing to do is detect and handle the (possibly) empty lists?"
]
},
{
"cell_type": "markdown",
"id": "d54e0860",
"metadata": {},
"source": [
"#### predicate"
]
},
{
"cell_type": "code",
"execution_count": 92,
"id": "728f7b72",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"true"
]
}
],
"source": [
"clear\n",
"\n",
"[1] [1] [bool] ii &"
]
},
{
"cell_type": "code",
"execution_count": 93,
"id": "3561502a",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false"
]
}
],
"source": [
"clear\n",
"\n",
"[1] [] [bool] ii &"
]
},
{
"cell_type": "code",
"execution_count": 94,
"id": "2c395fcc",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false"
]
}
],
"source": [
"clear\n",
"\n",
"[] [1] [bool] ii &"
]
},
{
"cell_type": "markdown",
"id": "13993d1f",
"metadata": {},
"source": [
"So our `ifte` predicate is `[bool] ii &`, what's the rest look like?\n",
"\n",
" [[bool] ii &] ... [add_digits] ... ifte\n",
"\n",
"We will need `add_digits` on the `true` branch to deal with the rest of the lists, but not (I think) on the false branch?\n",
"\n",
" [[bool] ii &] [... [add_digits] ...] [ELSE] ifte"
]
},
{
"cell_type": "code",
"execution_count": 130,
"id": "9caf15b4",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"[_add_rec_pred [bool] ii &] inscribe"
]
},
{
"cell_type": "markdown",
"id": "9445eb3c",
"metadata": {},
"source": [
"Plugging in `add-with-carry` we get:"
]
},
{
"cell_type": "code",
"execution_count": 118,
"id": "7e745018",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"5 false [2 3] [5 6]"
]
}
],
"source": [
"clear\n",
"\n",
"false [1 2 3] [4 5 6] uncons-two [add-with-carry] dipd"
]
},
{
"cell_type": "markdown",
"id": "121ff3c0",
"metadata": {},
"source": [
"### Recur\n",
"\n",
"It is at this point that we would recur:\n",
"\n",
" 5 false [2 3] [5 6] [add_digits] i ...\n",
" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ \n",
"\n",
"This part runs and becomes some list (possibly empty) of result digits (the base case consumes the carry flag and one list):\n",
"\n",
" 5 [7 9]\n",
"\n",
"So our conclusion must be `cons`:\n",
"\n",
" 5 [7 9] cons\n",
" [5 7 9]\n",
"\n",
"And our whole branch function is:\n",
"\n",
" THEN == uncons-two [add-with-carry] dipd [add_digits] i cons\n",
"\n",
" [_add_rec_pred] [THEN] [ELSE] ifte\n",
"\n",
"It's a little tricky having that recursive call being nested like that:\n",
"\n",
" THEN0.1 == [add-with-carry] dipd\n",
" THEN0 == uncons-two THEN0.1\n",
" THEN1 == i cons\n",
"\n",
" [_add_rec_pred] [THEN0 [add_digits] THEN1] [ELSE] ifte\n",
"\n",
"But we can make it work."
]
},
{
"cell_type": "markdown",
"id": "cd576704",
"metadata": {},
"source": [
"#### Interlude: Nested or Unnested?\n",
"\n",
" F == [P] [THEN] [R0] [R1] genrec\n",
" F == [P] [THEN] [R0 [F] R1] ifte\n",
"\n",
"Our recursive branch will take the form of an `ifte` expression that incorporates the function `[F]` into one of its branches:\n",
"\n",
" F == [P] [THEN] [[P0] [THEN0 [F] THEN1] [ELSE] ifte] ifte\n",
"\n",
" F == [P] [THEN] [[P0] [THEN0]] [F] [[THEN1] cons concat [ELSE] ifte] ifte\n",
"\n",
"\n",
"\n",
" [P0] [THEN0] [F] [THEN1] cons concat [ELSE] ifte\n",
" ------------------------------------------------------\n",
" [P0] [THEN0] [[F] THEN1] concat [ELSE] ifte\n",
" ------------------------------------------------------\n",
" [P0] [THEN0 [F] THEN1] [ELSE] ifte\n",
" ------------------------------------------------------\n",
" [P0] [THEN0 [F] THEN1] [ELSE] ifte\n",
"\n",
"It's awkward but it works."
]
},
{
"cell_type": "code",
"execution_count": 112,
"id": "4fcf1d97",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear"
]
},
{
"cell_type": "markdown",
"id": "aa76c2fc",
"metadata": {},
"source": [
"#### add-carry-to-digits\n",
"So now we have `carry` and one list of digits. (We also know that we have at least one digit in the list at this point but we likely won't need that information.)\n",
"\n",
" carry [a ...] add-carry-to-digits\n",
"\n",
"I think once we define `add-carry-to-digits` we are pretty much done? Let's find out."
]
},
{
"cell_type": "markdown",
"id": "828699dc",
"metadata": {},
"source": [
"##### If `carry` is `false` we just return the digits list, eh?\n",
"\n",
" false [a ...] swap [] [THEN] branch\n",
" -----------------------------------------\n",
" [a ...]"
]
},
{
"cell_type": "markdown",
"id": "2a386fe2",
"metadata": {},
"source": [
"##### If `true` we want to maybe reuse `add-with-carry`?\n",
"\n",
"\n",
" true [a ...] swap [THEN] [] branch\n",
" ----------------------------------------\n",
" [a ...] THEN\n",
" --------------------------------------\n",
" false 1 a add-with-carry [...] G\n",
" --------------------------------------\n",
" (1+a) carry [...] G\n",
" ------------------------------------------------\n",
" (1+a) carry [...] add-carry-to-digits cons\n",
" ------------------------------------------------\n",
" (1+a) [...] cons\n",
" ------------------------------------------------\n",
" [(1+a) ...]\n",
"\n",
"So `add-carry-to-digits` is a recursive function (not a `branch` after all.)"
]
},
{
"cell_type": "markdown",
"id": "08a149fa",
"metadata": {},
"source": [
"Omitting `ditch-empty-list` for the moment:\n",
"\n",
" THEN == [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
"\n",
" [a ...] THEN\n",
" [a ...] [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
" false 1 [a ...] uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
" false 1 a [...] [add-with-carry] dip [add-carry-to-digits] i cons\n",
" false 1 a add-with-carry [...] [add-carry-to-digits] i cons\n",
" (1+a) false [...] [add-carry-to-digits] i cons\n",
" (1+a) false [...] add-carry-to-digits cons\n",
" (1+a) [...] cons\n",
" [(1+a) ...]\n",
"\n",
"QED"
]
},
{
"cell_type": "code",
"execution_count": 64,
"id": "9f4ebfd9",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear"
]
},
{
"cell_type": "markdown",
"id": "afd8074b",
"metadata": {},
"source": [
"#### add-carry-to-digits, recursively\n",
"\n",
" carry [...] add-carry-to-digits\n",
"\n",
" carry [...] [P] [THEN] [R0] [R1] genrec\n",
"\n",
"So:\n",
"\n",
" P == swap not\n",
" \n",
"-or-\n",
"\n",
" P == pop not\n",
" \n",
"and\n",
"\n",
" THEN == popd\n",
"\n",
"That leaves:\n",
"\n",
" true [...] R0 [add-carry-to-digits] R1\n",
"\n",
"I am tempted to leave the transformation from the above form to\n",
"\n",
" true [...] popd [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
"\n",
"as the proverbial \"exercise for the reader\" but it's kinda trivial:\n",
"\n",
" R0 == popd [false 1] dip uncons [add-with-carry] dip\n",
" R1 == i cons\n",
"\n"
]
},
{
"cell_type": "code",
"execution_count": 65,
"id": "0c095d53",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"2 false [2 3]"
]
}
],
"source": [
"true [1 2 3] popd [false 1] dip uncons [add-with-carry] dip"
]
},
{
"cell_type": "code",
"execution_count": 66,
"id": "e793bd13",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"2 [2 3]"
]
}
],
"source": [
"popd"
]
},
{
"cell_type": "code",
"execution_count": 67,
"id": "e5d3966a",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[2 2 3]"
]
}
],
"source": [
"cons"
]
},
{
"cell_type": "code",
"execution_count": 73,
"id": "c8aec12d",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear\n",
"\n",
"[add-carry-to-digits [pop not] [popd] [popd [false 1] dip uncons [add-with-carry] dip] [i cons] genrec] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 74,
"id": "d290d896",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[2 2 3]"
]
}
],
"source": [
"true [1 2 3] add-carry-to-digits"
]
},
{
"cell_type": "code",
"execution_count": 75,
"id": "10cb7a1f",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[1 2 3]"
]
}
],
"source": [
"clear\n",
"\n",
"false [1 2 3] add-carry-to-digits"
]
},
{
"cell_type": "code",
"execution_count": 84,
"id": "89298766",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"true [2147483647 2147483647 2 3]"
]
}
],
"source": [
"clear\n",
"\n",
"true base -- dup [2 3] ccons"
]
},
{
"cell_type": "code",
"execution_count": 85,
"id": "af73db1b",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[0 0 3 3]"
]
}
],
"source": [
"add-carry-to-digits"
]
},
{
"cell_type": "markdown",
"id": "69f59f45",
"metadata": {},
"source": [
"E.g. 3299 + 1 = 3300"
]
},
{
"cell_type": "code",
"execution_count": 90,
"id": "00fa293e",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false [2147483647 2147483647 2 3]"
]
}
],
"source": [
"clear\n",
"\n",
"false base -- dup [2 3] ccons"
]
},
{
"cell_type": "code",
"execution_count": 91,
"id": "227a28f1",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[2147483647 2147483647 2 3]"
]
}
],
"source": [
"add-carry-to-digits"
]
},
{
"cell_type": "markdown",
"id": "50d06f33",
"metadata": {},
"source": [
"So that seems like it works."
]
},
{
"cell_type": "code",
"execution_count": 119,
"id": "7e735e04",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear"
]
},
{
"cell_type": "markdown",
"id": "b55599cb",
"metadata": {},
"source": [
"## Our Story So Far...\n",
" _add_p == [bool not] ii &\n",
" _add_then == pop swap [] [1 swons] branch\n",
" _add_rec_pred == [bool] ii &\n",
"\n",
" add_digits == [_add_p] [_add_then] [R0] [R1] genrec"
]
},
{
"cell_type": "markdown",
"id": "f515f498",
"metadata": {},
"source": [
"Where:\n",
"\n",
" R0 [add_digits] R1\n",
" -----------------------------------------------------\n",
" [_add_rec_pred] [ THEN ] [ELSE] ifte\n",
" -----------------------------------------------------\n",
" [_add_rec_pred] [THEN0 [add_digits] THEN1] [ELSE] ifte\n",
"\n",
" THEN0 == uncons-two [add-with-carry] dipd\n",
"\n",
" THEN1 == i cons\n",
"\n",
" ELSE == ditch-empty-list add-carry-to-digits"
]
},
{
"cell_type": "code",
"execution_count": 131,
"id": "348e377d",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"[THEN0 uncons-two [add-with-carry] dipd] inscribe\n",
"[THEN1 i cons] inscribe\n",
"[ELSE ditch-empty-list add-carry-to-digits] inscribe"
]
},
{
"cell_type": "markdown",
"id": "c3b2768f",
"metadata": {},
"source": [
"Recalling:\n",
"\n",
" [P0] [THEN0] [F] [THEN1] cons concat [ELSE] ifte\n",
" ------------------------------------------------------\n",
" [P0] [THEN0] [[F] THEN1] concat [ELSE] ifte\n",
" ------------------------------------------------------\n",
" [P0] [THEN0 [F] THEN1] [ELSE] ifte\n",
" ------------------------------------------------------\n",
" [P0] [THEN0 [F] THEN1] [ELSE] ifte"
]
},
{
"cell_type": "markdown",
"id": "2d58b809",
"metadata": {},
"source": [
"Ergo:\n",
"\n",
" R0 == [_add_rec_pred] [THEN0]\n",
" R1 == [THEN1] cons concat [ELSE] ifte\n",
"\n",
" add_digits == [_add_p] [_add_then] [R0] [R1] genrec\n"
]
},
{
"cell_type": "code",
"execution_count": 132,
"id": "2219756c",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"[_add_R0 [_add_rec_pred] [THEN0]] inscribe\n",
"[_add_R1 [THEN1] cons concat [ELSE] ifte] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 133,
"id": "80866347",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"[add_digits [_add_p] [_add_then] [_add_R0] [_add_R1] genrec] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 134,
"id": "51314100",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false [3 2 1] [8]"
]
}
],
"source": [
"false [3 2 1] [8] "
]
},
{
"cell_type": "code",
"execution_count": 135,
"id": "63a589cb",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[11 2 1]"
]
}
],
"source": [
"add_digits"
]
},
{
"cell_type": "code",
"execution_count": 136,
"id": "b5c5b50b",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[2147483647 11 2 1]"
]
}
],
"source": [
"base -- swons"
]
},
{
"cell_type": "code",
"execution_count": 137,
"id": "1c81b4bc",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false [2147483647 11 2 1] [23]"
]
}
],
"source": [
"false swap [23]"
]
},
{
"cell_type": "code",
"execution_count": 138,
"id": "cdd845ef",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[22 12 2 1]"
]
}
],
"source": [
"add_digits"
]
},
{
"cell_type": "code",
"execution_count": 142,
"id": "583a2390",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[2147483647] [1]"
]
}
],
"source": [
"clear base -- unit [1]"
]
},
{
"cell_type": "markdown",
"id": "defedd4b",
"metadata": {},
"source": [
"When i tried it it failed and inspection revealed that I had forgotten to set the initial carry value."
]
},
{
"cell_type": "code",
"execution_count": 144,
"id": "532967be",
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false [2147483647] [1]"
]
}
],
"source": [
"clear false base -- unit [1]"
]
},
{
"cell_type": "code",
"execution_count": 145,
"id": "e15c8b33",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[0 1]"
]
}
],
"source": [
"add_digits"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "84c6c958",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": 148,
"id": "ca5c95af",
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"false [2147483647 2147483647 2147483647 2147483647] [1]"
]
}
],
"source": [
"clear false base -- unit dup concat dup concat [1]"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "3a6960ea",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"id": "8c32715b",
"metadata": {},
"source": [
"#### I made a mistake in add-carry-to-digits\n",
"\n",
"The recursive branch:\n",
"\n",
" true [...] R0 [add-carry-to-digits] R1\n",
"\n",
"Must also deal with the case where the list is empty!\n",
"\n",
" true [] R0 [add-carry-to-digits] R1\n",
"\n",
"The `popd` is okay, but then we need a branch:\n",
"\n",
" R0 == popd ? [1 swons] [R0.t] branch\n",
" R0.t == [false 1] dip uncons [add-with-carry] dip\n",
"\n",
" R1 == i cons\n",
"\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "1b4b1302",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"id": "cab5271f",
"metadata": {},
"source": [
"#### add-carry-to-digits, recursively, TAKE TWO\n",
"\n",
" carry [...] add-carry-to-digits\n",
"\n",
" carry [...] [P] [THEN] [R0] [R1] genrec\n",
"\n",
" P == pop not\n",
" THEN == popd\n",
"\n",
"That leaves one of:\n",
"\n",
" true [...] R0 [add-carry-to-digits] R1\n",
"\n",
"-or-\n",
"\n",
" true [] R0 [add-carry-to-digits] R1\n",
"\n",
"It would be fun to just set `R1` to `ifte`\n",
"\n",
" true [] R0 [add-carry-to-digits] ifte\n",
"\n",
"Which means that `R0` must be a predicate and the \"then\" branch.\n",
"\n",
" true [] [bool not] [THEN] [add-carry-to-digits] ifte\n",
"\n",
"And I think `THEN` would just be:\n",
"\n",
" THEN == popd 1 swons\n",
"\n",
"\n"
]
},
{
"cell_type": "code",
"execution_count": 162,
"id": "955aed77",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear\n",
"[R0.t [false 1] dip uncons [add-with-carry] dip] inscribe\n",
"[add-carry-to-digits\n",
" [pop not]\n",
" [popd]\n",
" [[bool not] [popd 1 swons]]\n",
" [ifte]\n",
" genrec\n",
"] inscribe"
]
},
{
"cell_type": "markdown",
"id": "1ee5b941",
"metadata": {},
"source": [
"This is still broken because the "
]
},
{
"cell_type": "code",
"execution_count": 160,
"id": "8ca1f509",
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"true [2147483647 2147483647 2147483647 2147483647]"
]
}
],
"source": [
"clear true base -- unit dup concat dup concat"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "77e2e26f",
"metadata": {},
"outputs": [],
"source": [
"add-carry-to-digits"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "07a528bd",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "97ed01aa",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "dee054a6",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "f92eebb0",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "36e683fd",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"id": "91ffeec1",
"metadata": {},
"source": [
"#### add-carry-to-digits\n",
"\n",
"So `add-carry-to-digits` is a recursive function:\n",
"\n",
" carry [a ...] add-carry-to-digits\n",
"\n",
" carry [a ...] [P] [THEN] [R0] [R1] genrec\n",
"\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "dc5f3cba",
"metadata": {},
"outputs": [],
"source": [
"[pop not] [popd] [[bool not] [1 cons swap]] [ifte] genrec"
]
},
{
"cell_type": "markdown",
"id": "6201b301",
"metadata": {},
"source": [
"##### If `carry` is `false` we just return the digits list, eh?\n",
"\n",
" false [a ...] [pop not] [popd] [R0] [R1] genrec\n",
" -----------------------------------------------------\n",
" [a ...]"
]
},
{
"cell_type": "markdown",
"id": "2ffbb77c",
"metadata": {},
"source": [
"##### If `true` we want to maybe reuse `add-with-carry`?\n",
"\n",
" true [a ...] R0 [add-carry-to-digits] R1\n",
"\n",
"-or-\n",
"\n",
" true [] R0 [add-carry-to-digits] R1\n",
"\n",
"Um...\n",
"\n",
" true [] [bool not] [1 cons popd] [add-carry-to-digits] ifte\n",
"\n",
"\n",
" true [] [bool not] [1 cons popd] [add-carry-to-digits] ifte\n",
" true [] 1 cons popd\n",
" true [1] popd\n",
" [1]\n",
"\n",
"-or-\n",
"\n",
" true [a ...] [bool not] [1 cons swap] [F add-carry-to-digits] itfe\n",
" true [a ...] F add-carry-to-digits\n",
"\n",
"\n",
" true [a ...] F add-carry-to-digits\n",
" ---------------------------------------------------------\n",
" true 0 a add-with-carry [...] add-carry-to-digits\n",
"\n",
" \n",
" F == 0 swap uncons [add-with-carry] dip\n",
"\n",
"\n",
" true [a ...] [bool not] [1 cons swap] [add-carry-to-digits] [F] swoncat itfe\n",
"\n",
"\n",
"\n",
" true [a ...] [bool not] [1 cons swap] [add-carry-to-digits] [0 swap uncons [add-with-carry] dip] swoncat itfe\n",
"\n"
]
},
{
"cell_type": "code",
"execution_count": 162,
"id": "0ee18517",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear\n",
"[R0.t [false 1] dip uncons [add-with-carry] dip] inscribe\n",
"[add-carry-to-digits\n",
" [pop not]\n",
" [popd]\n",
" [[bool not] [popd 1 swons]]\n",
" [ifte]\n",
" genrec\n",
"] inscribe"
]
},
{
"cell_type": "markdown",
"id": "965cf4df",
"metadata": {},
"source": [
"Omitting `ditch-empty-list` for the moment:\n",
"\n",
" THEN == [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
"\n",
" [a ...] THEN\n",
" [a ...] [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
" false 1 [a ...] uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
" false 1 a [...] [add-with-carry] dip [add-carry-to-digits] i cons\n",
" false 1 a add-with-carry [...] [add-carry-to-digits] i cons\n",
" (1+a) false [...] [add-carry-to-digits] i cons\n",
" (1+a) false [...] add-carry-to-digits cons\n",
" (1+a) [...] cons\n",
" [(1+a) ...]\n",
"\n",
"QED"
]
},
{
"cell_type": "code",
"execution_count": 64,
"id": "1787863d",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear"
]
},
{
"cell_type": "markdown",
"id": "77eeace6",
"metadata": {},
"source": [
"#### add-carry-to-digits, recursively\n",
"\n",
" carry [...] add-carry-to-digits\n",
"\n",
" carry [...] [P] [THEN] [R0] [R1] genrec\n",
"\n",
"So:\n",
"\n",
" P == swap not\n",
" \n",
"-or-\n",
"\n",
" P == pop not\n",
" \n",
"and\n",
"\n",
" THEN == popd\n",
"\n",
"That leaves:\n",
"\n",
" true [...] R0 [add-carry-to-digits] R1\n",
"\n",
"I am tempted to leave the transformation from the above form to\n",
"\n",
" true [...] popd [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
"\n",
"as the proverbial \"exercise for the reader\" but it's kinda trivial:\n",
"\n",
" R0 == popd [false 1] dip uncons [add-with-carry] dip\n",
" R1 == i cons\n",
"\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "2a37982c",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "0c1ad90d",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "a184d47c",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "0343594a",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "e13c8b2e",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "e921d72a",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "2727bab9",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "3373be97",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "342e9982",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "7f655e89",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "611f40ff",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "bada9caa",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "fb66962d",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "6764903e",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "b4b10bfe",
"metadata": {},
"outputs": [],
"source": [
"[base 2147483648] inscribe\n",
"[valid_digit [0 >] [base <] &&] inscribe\n",
"[_add_p [bool not] ii &] inscribe\n",
"[_add_then pop swap [] [1 swons] branch] inscribe\n",
"[_add_rec_pred [bool] ii &] inscribe\n",
"[bool_to_int [0] [1] branch] inscribe\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\n",
"[uncons-two [uncons] ii swapd] inscribe\n",
"[ditch-empty-list [bool] [popd] [pop] ifte] inscribe\n",
"[add-carry-to-digits [pop not] [popd] [popd [false 1] dip uncons [add-with-carry] dip] [i cons] genrec] inscribe\n",
"[THEN0 uncons-two [add-with-carry] dipd] inscribe\n",
"[THEN1 i cons] inscribe\n",
"[ELSE ditch-empty-list add-carry-to-digits] inscribe\n",
"[_add_R0 [_add_rec_pred] [THEN0]] inscribe\n",
"[_add_R1 [THEN1] cons concat [ELSE] ifte] inscribe\n",
"[add_digits [_add_p] [_add_then] [_add_R0] [_add_R1] genrec] inscribe\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "11c66f4e",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "60cda31e",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "0852a374",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "c2c3f8f5",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "eb4d2dac",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "6c7f705e",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "8e69a883",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"id": "551b52de",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": 55,
"id": "3fb6905c",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[1] 2 false [2 3]"
]
}
],
"source": [
"[isnt_bigint\n",
"[first isnt_bool]\n",
"[rest [isnt_int] map]\n",
"cleave cons\n",
"] inscribe"
]
},
{
"cell_type": "code",
"execution_count": 56,
"id": "39b3d4bc",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[1] 2 false [2 3] [[!] [!-] [!=] [%] [&] [&&] [*] [+] [++] [-] [--] [/] [<] [<<] [<<{}] [<=] [<>] [<{}] [=] [>] [>=] [>>] [?] [abs] [add] [add-with-carry] [all] [anamorphism] [and] [any] [app1] [app2] [app3] [appN] [at] [b] [base] [binary] [bool] [bool_to_int] [branch] [ccccons] [ccons] [choice] [clear] [cleave] [clop] [cmp] [codi] [codireco] [concat] [cond] [cons] [digitalize] [dinfrirst] [dip] [dipd] [dipdd] [disenstacken] [ditch-empty-list] [div] [divmod] [down_to_zero] [drop] [dup] [dupd] [dupdd] [dupdip] [dupdipd] [enstacken] [eq] [first] [first_two] [flatten] [floordiv] [fork] [fourth] [gcd] [gcd2] [ge] [genrec] [getitem] [grabN] [grba] [gt] [help] [i] [ifte] [ii] [infra] [infrst] [inscribe] [isnt_bigint] [isnt_bool] [isnt_int] [isnt_stack] [le] [loop] [lshift] [lt] [make_generator] [manual] [map] [max] [min] [mod] [mul] [ne] [neg] [not] [nulco] [nullary] [of] [or] [over] [pam] [pm] [pop] [popd] [popdd] [popop] [popopd] [popopdd] [popopop] [pow] [pred] [primrec] [product] [quit] [quoted] [range] [range_to_zero] [reco] [remove] [rest] [reverse] [roll<] [roll>] [rolldown] [rollup] [rrest] [rshift] [run] [second] [select] [sharing] [shift] [shunt] [size] [sort] [spiral_next] [split_at] [split_list] [sqr] [stack] [stackd] [step] [step_zero] [stuncons] [stununcons] [sub] [succ] [sum] [swaack] [swap] [swapd] [swoncat] [swons] [tailrec] [take] [ternary] [third] [times] [to_bigint] [trace] [tuck] [unary] [uncons] [unique] [unit] [unquoted] [unswons] [valid_digit] [warranty] [while] [words] [x] [xor] [zip] [|] [||] [•]]"
]
}
],
"source": [
"words"
]
},
{
"cell_type": "code",
"execution_count": 57,
"id": "4c5edbfa",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": []
}
],
"source": [
"clear"
]
},
{
"cell_type": "code",
"execution_count": 58,
"id": "1e201000",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"2147483648"
]
}
],
"source": [
"1 31 <<"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "b310e739",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": 59,
"id": "fc53f72d",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"12 3"
]
}
],
"source": [
"clear\n",
"\n",
"123 10 divmod"
]
},
{
"cell_type": "code",
"execution_count": 60,
"id": "2cb7c88f",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"12 0 3"
]
}
],
"source": [
"base divmod"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "e7c36361",
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": 61,
"id": "005ac08e",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"\n",
"==== Help on divmod ====\n",
"\n",
"Similarly to pm (\"Plus or minus\") this function computes\n",
"both the\n",
"::\n",
"\n",
" a b divmod\n",
" ---------------------\n",
" a b div a b mod\n",
" ---------------------\n",
" q r\n",
"\n",
"Where: q * b + r == a\n",
"\n",
"---- end ( divmod )\n",
"\n",
"\n",
"12 0 3"
]
}
],
"source": [
"[divmod] help"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "6ebcf6d8",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Joypy",
"language": "",
"name": "thun"
},
"language_info": {
"file_extension": ".joy",
"mimetype": "text/plain",
"name": "Joy"
}
},
"nbformat": 4,
"nbformat_minor": 5
}
Reference in New Issue View Git Blame Copy Permalink