Functional Computation in Peano Arithmetic
This page collects some information related to Gödel numbering and its use in encoding and manipulating numbers, and some information related to the definition of quickly growing functions like the Ackermann function. These topics both relate to large numbers which are a bit of a passion of mine.
Contents
Building On Other Functions; Boolean Operations
Guess What — I Lied! (Reordering Items)
See Also
My separate page on Godel's first Incompleteness Proof
My separate page on Hofstadter's TNT (Typographical Number Theory)
The L Language
The language used here is similar to LISP, which others have also chosen for such purposes because of its similarity to the Church-Kleene Lambda calculus. I call it the L language with "L" referring to "LISP" and to contrast with the R language to be defined later.
Everything defined by this language is a function that takes zero or more arguments. Functions are defined in terms of primitives and other functions. The numeric constant 0 is a primitive as is the name of an argument. Primitives and functions are combined via pre-defined functions (also called operators), and incluing a function invocation as an argument to another function which can be thought of as an expression. With any given set of argument values, the function either has a definite, well-defined value or it has no defined value because it is infinitely recursive. All of the above is very similar to computer programming, and if a suitable LISP implementation were chosen, some of these functions might actually produce useful results in a managable amount of time. There are additional properties that are not like real computer languages: All values are non-negative integers, and all non-negative integers are values (that is, there is no limit to the size of the integers), and there is no concern for how long a function might take to return a value, so long as it is provably finite.
Parentheses are used to delineate arguments and subexpressions. Any function name is any sequence of letters, numbers, "_" and "-" that is not one of the three predefined operator names. Uppercase letters are considered equivalent to their lowercase counterparts, and "_" is considered equivalent to "-". Thus, the function names "Times-2" and "times_2" both refer to the same function and can be used interchangably to suit the user's taste. If a function name appears outside parentheses, it begins a function definition; any other function name is a call to the function. The complete function definition consists of the function name, a (, the names of its arguments if any, a ), another (, a single predefined operator or function name followed by its arguments if any, and a ). As mentioned previously, any argument can be a primtive 0, a parameter, or another function invocation contained within parentheses. Functions may call themselves or other functions whose definition appears anywhere else in the source text. All of this will be clear in the examples to follow.
The only predefined primitive is 0. The predefined functions (or "operators") are:
(inc a) : Returns a+1.
(dec a) : Returns a-1, or 0 if a=0.
(if a b c) : If a is non-zero, returns b, otherwise returns c.
In the foregoing, "a", "b" and "c" can be bare letters, referring to an argument of the function currently being defined, or they can be parentheses containing a predefined operator or a function invocation followed by its arguments. This is the only way to include more than one operation in a function. Typically functions use nested ifs as in LISP programming. In addition, and independently of all the syntax defined so far, a semicolon ; and any text after it on a line is ignored (providing a way for the author to include comments and explanations).
Readers experienced with the Peano axioms should recognize that they have nothing like "decrement" or "predecessor". However they do have "equality" which we are not using. I discuss this below in the section on Alternative Axioms.
The First Four Functions
Without further ado, here are the four most familiar arithmetic operators (modified where necessary to comply with the limitation of non-negative integer values). If you can understand these, then you've pretty much learned the language.
plus (a b) ; returns a+b (if a (plus (dec a) (inc b)) b ) minus (a b) ; returns a-b, or 0 if b>a. (if a (if b (minus (dec a) (dec b)) a ) 0 ) times (a b) ; returns a*b (if a (if b (plus (times (dec a) b) b) 0 ) 0 ) div (a b) ; returns a/b (rounded down). If b=0 it will never return! (if (minus (inc a) b) (inc (div (minus a b) b)) 0 )Integer Constants
Attentive readers might realize that the L language allows defining a number like "3" as a function name. This was deliberate, because it allows defining integer constants. It also allows very confusing function definitions if misused, but we're only going to use them in the obvious way:
1 () (inc 0) 2 () (inc (1)) 3 () (inc (2))Notice that the parentheses are needed around these defined constants, because each is actually defined as a function that takes zero arguments.
Building On Other Functions
The first two basic functions (plus and minus) stand by themselves — they don't call another function to accomplish their results. The other two represent the more common situation, where a function builds on another function (times calls plus, and div calls minus). All four functions also call themselves recursively.
Here are some more basic operations that are very useful and can be accomplished very easily with the functions we just defined:
not-arith (a) ; boolean NOT function, treats any nonzero argument as true ; and always returns 0 or 1. (minus (1) a) and-arith (a b) ; boolean AND function, treats any nonzero argument as true ; and always returns 0 or 1. (minus (1) (minus (1) (times a b))) or-arith (a b) ; boolean OR function, treats any nonzero argument as true ; and always returns 0 or 1. (minus (1) (minus (1) (plus a b))) lt (a b) ; returns a nonzero result if a<b (minus b a) gt (a b) ; returns a nonzero result if a>b (minus a b) le (a b) ; returns a nonzero result if a≤b (minus (inc b) a) ge (a b) ; returns a nonzero result if a≥b (minus (inc a) b) eq (a b) ; returns a nonzero result if a=b (minus (1) (plus (minus a b) (minus b a))) ne (a b) ; returns a nonzero result if a is not equal to b (plus (minus a b) (minus b a))All of the above are "boolean-valued" functions, in that they are intended to return 0 for a "false" answer and non-zero for "true". The first three always return 1 for "true". Having a specific value for "true" can be useful, but it's almost just as easy to treat any nonzero value as "true". The first three functions show how easy it is to accept any nonzero value as "true" for input purposes, and the other functions show how much simpler it is to produce boolean results when any nonzero value counts as "true".
These functions also demonstrate a very important principle, which is using addition, subtraction and multiplication as a way around explicit testing — note the lack of the if operator in any of the above. This results from several similarities between the boolean operators and their arithmetic counterparts, which are also reflected in some shared properties like associativity and commutativity. (Of course, they all use minus, which uses if — but if plus, minus and times were built in, we would be able to define all of these boolean and conditional operators without if).
For the purists, more conventional implementations of and and not based on explicit testing are shown below.
Alternative Axioms
In the title of the article I describe this as functional computation with Peano arithmetic. There is a zero and an "increment" function, and our (if a b c) operation is what makes this "computation". But there is no "decrement" function in the Peano axioms, however they do define "equality". If we have an equality function then (dec a) can be defined in terms of the givens by:
(dec a) : (if a (dec2 0 a) 0) (dec2 a b) : (if (equal (inc a) b) a (dec2 (inc a) b) )Conversely, our language does not some with an (equal a b) function. We just defined (eq a b) above, but we used dec for that. We could have instead started out right from the start, defining an equality function this way:
(equal a b) : (if a (if b (equal (dec a) (dec b)) 0) (if b 0 1) )This sort of thing is common in axiomatic systems. Many alternative sets of axioms can be equivalent. Mathematicians have their reasons for choosing a particular set, I chose inc, dec and if because they make it easier to get started with arithmetic.
Now we get to do some more interesting things. First, let's consider Gödel numbering.
Gödel Numbering
Gödel numbering is used in his first incompleteness theorem
The basic principle of Gödel numbering is to "encode" two or more numbers in a single numeric quantity. (For now, let's not worry about why someone would want to do such a thing.)
The "fundamental theorem of arithmetic" states that every number has exactly one, unique and distinct prime factorization — and every prime factorization multiplies out to exactly one unique and distinct numeric value. More specifically, the expression 2m3n has a distinct value for every combination of m and n. Thus, a single number x=2m3n can be used to represent two different and possibly completely unrelated numbers m and n.
Let's say we want to define a function that takes such a number x and returns a value y=2p3q. Such a function would need to take its arguments m and n and perform operations analogous to the builtin operations inc, dec and if separately on m and n. This can be accomplished by defining a set of six functions:
(inc-enc1 x) ; Increment the first encoded value in x — that is, given x=2m3n, returns 2m+13n.
(dec-enc1 x) ; Decrement the first encoded value in x — that is, given x=2m3n, returns 2m-13n, or 3n in the case where m is zero.
(if-enc1 x a b) ; Like if, but dependent only on the first encoded value in x — that is, given x=2m3n, returns a if m is greater than zero, and b otherwise.
and three "-enc2" functions defined similarly. Here is the implementation:
inc-enc1 (x) ; increment the first quantity encoded in the argument (times x (2)) inc-enc2 (x) ; increment the second quantity encoded in the argument (times x (3)) odd (x) ; returns a nonzero result if x is odd (if x (if (dec x) (odd (dec (dec x))) x ) 0 ) dec-enc1 (x) ; decrement the first quantity encoded in the argument (if (odd x) x (div x (2)) ) not-div3 (x) ; returns a nonzero result if x is not divisible by 3 (if x (if (dec x) (if (dec (dec x)) (not-div3 (dec (dec (dec x)))) (1) ) x ) 0 ) dec-enc2 (x) ; decrement the second quantity encoded in the argument (if (not-div3 x) x (div x (3)) ) if-enc1 (x a b) ; test the first quantity encoded in the argument x (which is treated ; as x=2m3n), if that quantity m is nonzero, return a, ; else return b (if (odd x) ; x is odd, so m is zero, so we return b b ; x is even, so m is 1 or more, so we return a a ) if-enc2 (x a b) ; test the second quantity encoded in the argument x (which is treated ; as x=2m3n), if that quantity n is nonzero, return a, ; else return b (if (not-div3 x) ; x is not divisible by 3, so n is zero, so we return b b ; x is a multiple of 3, so n is 1 or more, so we return a a )Note that the last two functions, if-enc1 and if-enc2, take 3 arguments and work like the builtin if. If we wish, we can define one-argument functions and use the if operator itself. To do that, we define:
nonzero-enc1-p (x) ; Given x=2m3n), return a nonzero result if and only if ; m is nonzero. (not (odd x)) nonzero-enc2-p (x) ; Given x=2m3n), return a nonzero result if and only if ; n is nonzero. (not (not-div3 x))With these definitions, the expression (if (nonzero-enc1-p x) a b) is equivalent to (if-enc1 x a b), and likewise for nonzero-enc2-p and if-enc2, and we've done it without defining a function that takes more than two variables.
Arbitrary Indexing
True Gödel numbering requires an arbitrary index function:
(inc-enc-n x n) ; Given x=2j3k5l7m..., increments the nth exponent and returns the result.
(dec-enc-n x n) ; Given x=2j3k5l7m..., decrements the nth exponent (unless that exponent is already zero) and returns the result.
(if-enc-n x n a b) ; Given x=2j3k5l7m..., returns a if the nth exponent is greater than zero, and b otherwise.
For this we have to actually generate and test for arbitrary prime numbers:
divisible (a b) ; return a nonzero result if a is divisible by b, otherwise return 0 ; in addition we return 0 if b is zero, just to make the function more ; useful. (if b (if (minus a (times (div a b) b)) ; a is greater than (a/b)×b, so a is not divisible by b 0 ; a=(a/b)×b, so we return 1. (1) ) 0 ) not (a) ; boolean NOT function, treats any nonzero argument as true ; and always returns 0 or 1. (if a 0 (1) ) and (a b) ; boolean AND function, treats any nonzero argument as true ; and always returns 0 or 1. (if a (if b (1) 0 ) 0 ) prime-upto (a b) ; return 1 if and only if a is not divisible by any numbers less than or ; equal to b. Divisibility by 1 does not count. (if b (if (dec b) ; b is 2 or more. result is true if a is not divisible by b AND ; prime-upto for all numbers less than b. (and (not (divisible a b)) (prime-upto a (dec b)) ) ; b is 1, we treat this as a true case b ) ; b is zero, we treat this as a true case (1) ) prime-p (a) ; return a nonzero result if a is prime; treats 0 and 1 as not prime. (if a (if (dec a) (prime-upto a (dec a)) 0 ) 0 ) next-prime (a) ; returns the smallest prime greater than a (if (prime-p (inc a)) (inc a) (next-prime (inc a)) ) nth-next-prime (a n) ; returns the nth next prime after a. If n=1, this is the same as ; next-prime above; if n=0, just returns a which of course might not ; itself be prime. (if n (nth-next-prime (next-prime a) (dec n)) a ) nth-prime (n) ; return the nth prime number pn, defined as p0=0, p1=2, ; p2=3, p3=5, etc. (nth-next-prime 0 n)Having defined all of this, the manipulation functions for the nth encoded value can be defined in almost the same way as the simpler examples above:
inc-enc-n (x n) ; increment the nth quantity encoded in the argument (times x (nth-prime n)) dec-enc-n (x n) ; decrement the nth quantity encoded in the argument (if (not (divisible x (nth-prime n))) x (div x (nth-prime n)) ) if-enc-n (x n a b) ; test the nth quantity encoded in the argument, if it is nonzero ; return a, else return b (if (not (divisible x (nth-prime n))) ; x is not divisible by pn, so the encoded quantity is zero, ; so we return b b ; other case, return a a )Again we have defined one function (if-enc-n) that takes more than two arguments, but as before, we can replace it with a two-argument alternative:
nonzero-enc-n-p (x n) ; Return a nonzero result if the nth quantity encoded in the ; argument x is nonzero. (divisible x (nth-prime n))and the expression (if (nonzero-enc-n-p x n) a b) is equivalent to (if-enc-n x n a b).
Arbitrary Reordering
Actually, there is one more important operation that a function might need to perform on Gödel-encoded values, and that is illustrated by the following function, which has been intentionally written in an overly complex way:
maxval-clumsy (a b) ; returns a if a>b, otherwise returns b (if (minus (inc a) b) a (maxval-clumsy b a) )The above function calls itself, with the arguments reversed. This is actually the first place so far that I have defined a function that calls itself with the arguments in a different order. Although this example is unnecessary, there are (rare) cases in which reordering arguments is important.
So, with respect to Gödel-numbering, the additional operation we need to be able to do is to rearrange encoded values: given x=2a3b, compute y=2b3a, and similar operations for reordering three or more values.
expt (a b) ; returns ab. We return 0 for 0^0. (if a (if b (times b (expt a (dec b))) (1) ) 0 ) ilog (a b) ; returns log of a to base b (rounded down). If b=0 it will ; never return! (if (lt a b) 0 (inc (ilog (div a b) b)) ) logmod (a b) ; returns the number of exponents of b (which should be prime) that are ; in a. That is, if a=bp×n, returns p; if a is not ; divisible by b, returns 0. (if (divisible a b) (inc (logmod (div a b) b)) 0 ) goedel-extract (x n) ; extracts the nth Gödel-encoded component of x (logmod x (nth-prime n)) exchange-2 (x) ; given x=2a3b, returns y=2b3a. (times (expt (2) (goedel-extract x (2))) (expt (3) (goedel-extract x (1))) )We're partway there — we can extract values, and perform simple reordering as demonstrated by exchange-2. We also need to be able to manipulate entire groups of encoded values in a single operation:
factor-out (a b) ; Returns a/b^n, where n is the highest integer for which b^n divides evenly ; into a (if (divisible a b) (factor-out (div a b) b) a ) pr-list-2 (x b) ; Given x=2a3b...pcrd..., return ; 3a5b...qcrd q represents the next prime after ; p and b≤p. In other words, this moves all encoded values "to ; the right" in the factorization, up to and including the encoded value ; that is encoded in base b or the largest prime smaller than b. (if (dec b) ; b is 2 or more (if (prime-p b) (pr-list-2 (times (factor-out x b) (expt (next-prime b) (logmod x b)) ) (dec b) ) (pr-list-2 x (dec b)) ) ; b is 0 or 1 — we're done x ) promote-list (x) ; Move all encoded values one space "to the right" in the encoding. (pr-list-2 x x) prev-prime (a) ; Return the prime previous to a, or 0 if there is no such prime. (if a (if (prime-p (dec a)) (dec a) (prev-prime (dec a)) ) 0 ) de-list-2 (x b) ; Given x=3a5b...pcrd, return ; 2a3b...pcqd... where q represents the next prime ; after p and b≤q. In other words, this moves all encoded values "to ; the left" in the factorization, starting with the encoded value ; that is encoded in base b or the next prime after b. If b is less ; than 3, the value encoded in 2a will be lost. (if (lt x b) ; b>x, so we're done x (if (eq b (2)) ; b is 2, just remove this item and move up to the next b (de-list-2 (factor-out x b) (inc b)) ; b is something else, test for prime (if (prime-p b) ; b is prime, move this item down one (de-list-2 (times (factor-out x b) (expt (prev-prime b) (logmod x b)) ) (inc b) ) ; b is not prime, just go to the next b. (pr-list-2 x (inc b)) ) ) ) demote-list (x) ; Move all encoded values one space "to the left" in the encoding. Anything ; encoded in the first space (2a) will be lost. (de-list-2 x 0)Lists of Lists
We are now in a position to conveniently implement the most fundamental primitive operators of the LISP programming language, car, cdr and cons:
car (l) ; Return the first item in the list encoded by l (logmod l (2)) cdr (l) ; Return a list containing all the items in the list encoded by l but ; with the first item removed. (demote-list l) cons (a l) ; Add the value in a to the beginning of the list encoded by l, ; returning a list with one more element. Note that a can itself encode ; a list, in which case the result can be interpreted as a list whose ; first item is a list. This enables us to build lists of lists, nested ; arbitrarily deep. Note also that you create a list of one item with ; (cons a 0), and you create a list of two items with (cons a (cons b 0)), ; not (cons a b). (times (expt (2) a) (promote-list l) ) list1 (a) ; Creates a list with just a single item (Like the LISP function list ; with one argument) (expt (2) a) list2 (a b) ; Creates a list with two items (Like the LISP function list with two ; arguments) (times (expt (2) a) (expt (3) b) )The R Language
I am now going to define a subset of the L language we have been using so far, and call it the R language. "R" is intended to stand for "recursive", or could also be "reduced".
The primary "reduction" of the R language as compared to the L language is that each function always fits the following template:
r-function (arg1 arg2 arg3 ...) (if arg1 r-expa r-expb )r-exp-a and r-exp-b are R-expressions. Each R-expression must be one of the following:
0 arg (inc r-exp) (dec r-exp) (function r-exp r-exp r-exp ...)This is similar to the definition of expressions in the L language, except that if is not allowed inside expressions. Thus, the only place if can appear is at the beginning of a function definition, and it always appears there.
To translate L language functions to R language, two types of changes must be made:
- Any function that contains a single expression (and no if) can be rewritten as (if 0 0 (expr)) where (expr) is the original definition of the function
- Any function that contains a nested if needs to be rewritten into two or more functions, typically with one new function for each if in the original L language function.
A combination of these two techniques is used for functions that contain if but do not begin with it.
This can best be illustrated with examples. The following examples represent a subset of the above functions defined in L language. Each function name is preceded with R- and produces the same result as its counterpart above. For example, R-minus gives the same result as minus.
R-plus (a b) ; This is an example of a function that needs no changes whatsoever. (if a (R-plus (dec a) (inc b)) b )%%% (incomplete section)
The R-Machine
Now we define a Turing machine that is designed to evaluate R-functions.
%%% (incomplete section)
Operation of the R-Machine
Example 1: A Trivial Case
The marker begins at the end of the expression to be calculated:
3 [M] D: foo 0 t: p.0 f: 0
The machine scans to the left for the last function-name:
[M] 3 D: foo 0 t: p.0 f: 0
There is no function-name in the input, so the machine halts. The output is located to the right of the current position, which is at [M], and the output ends just before DEF:.
Example 2: A Single Function
The marker begins at the end of the expression to be calculated:
f.plus 3 4 [M] DEF: plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans to the left for the last function-name:
[M] f.plus 3 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine searches for the function's definition. [R] is a marker used for reading a function definition:
f.plus [M] 3 4 DEF:plus [R] 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine removes the function keyword from the input:
[M] 3 4 DEF:plus [R] 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine tests the first argument and finds that it is nonzero. This scans [M] across the "3" and back.
The machine scans ahead to the t: clause of the function definition:
[M] 3 4 DEF:plus 0 1 t: [R] f.plus D p.0 I p.1 f: p.1
The machine copies the t: clause into the input, shifting everything to the right one space at a time. This introduces another temporary marker [W] used for writing.
[M] f.plus D p.0 I p.1 [W] 3 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 [R] f: p.1
A marker [P] is added to remember where the parameters are:
[M] f.plus D p.0 I p.1 [WP] 3 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 [R] f: p.1
The machine scans [W] backward for a parameter selector:
[M] f.plus D p.0 I [W] p.1 [P] 3 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 [R] f: p.1
[R] is moved to the beginning of the parameters:
[M] f.plus D p.0 I [W] p.1 [PR] 3 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
[R] is moved to the beginning of the parameter that is needed:
[M] f.plus D p.0 I [W] p.1 [P] 3 [R] 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
"p." is removed, and the parameter value is copied:
[M] f.plus D p.0 I 4[W] [P]3 4[R] DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans [W] backward for a parameter selector:
[M] f.plus D [W] p.0 I 4 [P] 3 4 [R] DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
[R] is moved to the beginning of the parameters:
[M] f.plus D [W] p.0 I 4 [PR] 3 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
[R] is moved to the beginning of the parameter that is needed (this time, not moving at all):
[M] f.plus D [W] p.0 I 4 [PR] 3 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
"p." is removed, and the parameter value is copied:
[M] f.plus D [W] 3 I 4 [P] 3 [R] 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans [W] backward for a parameter selector, and reaches [M]. This signals the end of substitution and [M] and [W] are both removed:
{} f.plus D 3 I 4 [P] 3 [R] 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans for [R], removes it, then scans for [P]:
f.plus D 3 I 4 {[P]} 3 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine deletes the parameters:
f.plus D 3 I 4 {[P]} DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine replaces [P] with [M]:
f.plus D 3 I 4 {[M]} DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans to the left for a function:
f.plus D 3 [M] I 4 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The function is the builtin Increment function. The machine increments the following quantity and then removes I:
f.plus D 3 [M] 5 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans to the left for a function:
f.plus [M] D 3 5 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The function is the builtin Decrement function. The machine decrements the following quantity and then removes D:
f.plus [M] 2 5 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans to the left for a function:
[M] f.plus 2 5 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
Computation proceeds as in the above 20-plus steps, until it has just finished decrementing a "1" to "0":
f.plus [M] 0 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans to the left for a function:
[M] f.plus 0 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine searches for the function's definition. [R] is a marker used for reading a function definition:
f.plus [M] 0 7 DEF:plus [R] 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine removes the function keyword from the input:
[M] 0 7 DEF:plus [R] 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine tests the first argument and finds that it is zero. This scans [M] across the "0" and back.
The machine scans ahead to the f: clause of the function definition:
[M] 0 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: [R] p.1
The machine copies the f: clause into the input, shifting everything to the right one space at a time. This introduces another temporary marker [W] used for writing.
[M] p.1 [W] 0 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: [R] p.1
A marker [P] is added to remember where the parameters are:
[M] p.1 [WP] 0 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: [R] p.1
The machine scans [W] backward for a parameter selector:
[MW] p.1 [P] 0 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: [R] p.1
[R] is moved to the beginning of the parameters:
[MW] p.1 [PR] 0 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
[R] is moved to the beginning of the parameter that is needed:
[MW] p.1 [P] 0 [R] 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
"p." is removed, and the parameter value is copied:
[M]7[W] [P]0 7[R] DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans [W] backward for a parameter selector, and reaches [M]. This signals the end of substitution and [M] and [W] are both removed:
{}7 [P]0 7[R] DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans for [R], removes it, then scans for [P]:
7 {[P]}0 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine deletes the parameters:
7 {[P]}DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine replaces [P] with [M]:
7 {[M]}DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
The machine scans to the left for a function and finds none:
{[M]} 7 DEF:plus 0 1 t: f.plus D p.0 I p.1 f: p.1
There is no function-name remaining in the input, so the machine halts. The output is located to the right of the current position, which is at [M], and the output ends just before DEF:.
This page was written in the "embarrassingly readable" markup language RHTF, and was last updated on 2013 Feb 26.
s.27