Underload

Underload

Paradigm(s)	"functional"
Designed by	User:ais523
Appeared in	2006
Computational class	Turing complete
Major implementations	See below
Influenced by	Muriel
Influenced	Numeric Underload, CJam-Flavored Underload, Fueue, Clementine, Tarski, sorry, srry
File extension(s)	.ul

Underload is a stack-based esoteric programming language that works along similar lines to Muriel. It was created by User:ais523 in 2006. Although not technically speaking a functional language, its evaluation operator ^ (which is the only form of flow control) makes programming in it functional in practice.

Reserved characters

The bracket and angle bracket characters []<> are reserved; if these are to appear anywhere in the program, they must be quoted by placing " before them. This also applies to the " character itself. Other characters must not be quoted with " (in particular, this means that Underload programs cannot output strings containing unmatched parentheses). Parentheses are moderately reserved, in that any Underload program must have matched parentheses to be legal. However, no known interpreter ever, not even the reference interpreter, seems to have implemented any part of this other than the rules about parentheses, and this is therefore arguably not part of the language.

Commands

command : stack before — stack + remaining program after

Describes commands here.

---

~ : (x) (y) — (y) (x)

Swap the top two elements of the stack.

: : (x) — (x) (x)

Duplicate the top element of the stack.

! : (x) —

Discard the top element of the stack.

* : (x) (y) — (xy)

Concatenate the top element of the stack to the end of the second element of the stack.

(x) : — (x)

Push everything between the ( and the matching ) on top of the stack.

a : (x) — ((x))

Enclose the top element of the stack in a pair of parentheses.

^ : (x) — x

When the ^ command is called, include the top element of the stack into the program rather than the stack, immediately after the ^ command, ready to be run next; this effectively pops the stack.

S : (x) —

Output the top element of the stack, popping it.

Exceptional circumstances

Pretty much anything whose behaviour isn't specifically given here (for instance, running * on an empty stack) is an error.

Examples

99 bottles of beer

Available here.

Factorial

(outputs the factorial of however many colons are in the first set of parentheses)

(:::::::):(:((^:()~((:)*~^)a~*^!!()~^))~*()~^^)~(^a(*~^)*a~*()~^!()~^)a~**^!!^S

Fibonacci sequence

The first Fibonacci sequence for Underload used unary:

(()(*))(~:^:S*a~^a~!~*~:(/)S^):^

Here is one using the below decimal printing method:

(:(1)*(:(2)*(:(3)*(:(4)*(:(5)*(:(6)*(:(7)*(:(8)*(:(9)*(!~:^)))))))))):(
)!(~^~(~a~*~a~*)~a*^:(0)*)~a*~:(a(:^)*())~*a(:^)*~()~(0)((!^~)())(
)!((:(~:(,)*S~^!^)~a*^:^~!a~^*a*)~a*^:^):^

Kolakoski sequence

(12)S(*a(~:)~*^~):((1)S)~*~((2)S:*)~*:(~:()~)~*^(a(:^)*~a(*()~)~*^~^):^

Thue-Morse sequence

(0)S((0)(1))(~:^:S*a~^~*a*~:^):^

Print a numeral as decimal

The following can also be adjusted to produce strings for 0, 1, 2, ... etc. iteratively. (Which it does internally anyway.)

(:*)::::****:*(<-- Sample numeral (1024) to be printed
)!((:(1)*(:(2)*(:(3)*(:(4)*(:(5)*(:(6)*(:(7)*(:(8)*(:(9)*(!~:^))))))))))(
)!:(~^~(~a~*~a~*)~a*^:(0)*)~a*~:(a(:^)*())~*a(:^)*~()~(0)~(~!^))~*^^!S!!!

Look-and-say sequence

See also design scratch file.

((::**)~^)(<-- Initial number as sequence of encoded digits each followed by ~^
)!((((:(((((((((((_)(9))(8))(7))(6))(5))(4))(3))(2))(1))(0)(!^))~*^^S!)(
)!(:a(~^)*~(()(~(~(:a~*):^))(a))~*^^)):^(()~)~**~^(:)~((a(~^)*~**)~a)~a(
)!(**~:((:)~(*)**)~a*~(^))**a(~*^^^!!^)***(~)~a(~a*^:)**a(:)**~^!!!a(~^)*~**)(
)!~a((, )S:^)**^):^

Hello, world!

(Hello, world!)S

Infinite loop

(:^):^

Rule 110 cellular automaton

(^^:^^^:^^^^^:^^^^^^:::^^^^^^^^:::^^^:^^^^::^)(<-- Initial automaton state
)!()~((())~:a~*):a~*~^!(~((!())(!:^(^)*)(!!:^(!^)*))~*^!!^):^(
)!(~((()())(:a~*:(*(!^)(:)S)~*~(!*(^)(^)S)~*):a~**((!^)~^!^)(!(^)~^^))~*^(
)S!!a:(*)*~(~*)**^~*(()()(!)()(!)(:a~*:(!^(!^((!^)*)(!(^)*))(!^((^)*)(!(^)*)))(
)!~*~(!^(!^((!^)*)(!(^)*))(!^((^)*)(!(!^)*)))~*):^)~*^!!!!!!~:^):^

Binary counting Turing machine

The following program implements a 3 states, 3 symbols Turing machine to count in binary, while containing none of the commands *a. It can be expanded to a 3250 characters equivalent program which does not contain ! either.

(( )S)(^!!)(((~:^~(~)S(^!!)~(^)~:^^)(!~(:^!^)~^^^)(!!~(:^!!^)~^^!^))(
)!(!(~:^~(^!!)~:^^)(!~(:^!^)~^^!^)(!!~(:^!^)~^^^))(!!(~(:^!!^)~^^!!^)(
)!(!(:)S(^!)~:^^)(!!(~)S(^)~:^^))):^^!^!!^

Reverse binary printing Minsky machine

The following program implements a two-counter Minsky machine to print a number (given by the long string of ^'s) in reverse binary without using the commands ~*a.

(((((0)S!:^^^!^)(!:^!^))(!((1)S!:^^^!^)(!::^!!^))(!!(!:^^^^)))(
)!(((0)S)())(!((1)S)(!:^!!^))(!!(!:^!^))):^^(^^^^^^^^^^^^^^^^^^^^^^^^^^^)^!^

Quine

(a(:^)*S):^

(:aSS):aSS

Palindromic quine

(:aS(:^S^:)Sa:):^S^:(:aS(:^S^:)Sa:)

Looping counter

()(~(*)*:(
)*S~:^):^

Alternately

(
)(~(*)~*:S~:^):^

Programming in Underload

Ignoring the never supported reserved characters, any string with matching parentheses is a usable Underload element, which can be printed using the S command. However there is no way to take apart an arbitrary element into its constituent characters. The only way to analyze the contents of a string element is by running it with the ^ command, which of course can have wildly varying effects and will in most implementations give an error if any character other than the nine command characters is executed.

Therefore, the only way to have data in Underload usable for anything other than print formatting is to encode it as subprograms using the commands of the language. Fortunately, although the result is rarely readable without great effort, the language has the means to do so in flexible ways.

Numbers

Underload has a convenient way to represent natural numbers, which even influences the naming of some of its commands, and which is inspired by the Church numerals of lambda calculus. A natural number n is represented as a program which takes the top element of the stack, and replaces it by n concatenated copies of itself. For example, ::** represents the number 3:

(test string)::** = (test stringtest stringtest string)

Any program which has this effect is a numeral. Some short representations of small numbers are:

0 !()         5 ::*:**
1 (empty)!    6 ::**:*
2 :*          7 :::**:**
3 ::**        8 :*:*:*
4 :*:*        9 ::**::**

For a longer list, see Underload/Numbers.

The connection with Church numerals appears when the resulting string is itself run as a program with ^: It corresponds to running the original program n times.

The * and ^ commands are named for their effect when they are applied to elements that are themselves numerals: * is multiplication and ^ is exponentiation.

(::**)(:*)* = (::**:*)

multiplies 3 and 2 to give 6, while

(:*)(:*:*:*)^

puts a numeral for 2⁸ = 256 on the stack.

Addition doesn't have its own command, but can be given as

(~)~**(:)~*(*)*

Although numerals are convenient and relatively compact to write, large ones can be inefficient to use since they greatly expand the string they are applied to.

Lists and tuples

Lists of general elements

The simplest way of combining several Underload elements into one is to put parentheses around the whole bunch: The elements (x), (y) and (z) combine into the single element ((x)(y)(z)), which contains a subprogram which will push all of the elements onto the stack.

This method works for a list with a known, finite number of elements, but will have hard to handle stack effects when the length of the list is unknown. One possible way of solving this is to put the length of the list as a numeral on top of the stack, although I have found other methods easier so far.

If you need to iterate over a list of unknown but still finite length, a convenient representation is

((x)~^(y)~^(z)~^)

This representation assumes that there is a subprogram on the top of the stack to handle a single element. After it has done so, it should put a new copy of itself (or possibly a different subprogram to handle the next element) back on top. For example, the following prints xyz by iteration:

(S:):((x)~^(y)~^(z)~^)^

Another list representation uses nested pairs of first element / rest of list (essentially cons cells, for people familiar with Lisp). This representation has the advantage that it can be made infinite, by using a self-duplicating subprogram for generating the nesting. For example, the following acts as an infinite stream of (x)'s and a loop to print it:

((:a~*(x)):a~*(x))(~^S~:^):^

Tags and lookup tables

A convenient way to do branching in Underload is to use a list as a lookup table. It is then also convenient to let the chosen element perform the action of removing the other ones remaining on the stack. When doing this, after putting the list elements on the stack lookup can be done with ^, !^, !!^ etc. This makes the latter excellent representations for tags/enums and booleans. For example, the following selects the (y) element and prints it:

(((x))(!(y))(!!(z)))^!^S

Converting numerals to this tag form is also easy, although using this requires the numerals to be bounded by the table size. The following prints the numeral 5 by selecting the subprogram to print its digit from a table:

(((9)S)(!(8)S)(!!(7)S)(!!!(6)S)(!!!!(5)S)(!!!!!(4)S)(!!!!!!(3)S)(!!!!!!!(2)S)(!!!!!!!!(1)S)(!!!!!!!!!(0)S))^(!)(::*:**)^^^

Lists of tags

The above representations give lists of general elements. When the elements are tags in the !!!^ form one can simply concatenate them for a more compact iterable list. The following combines this with a self-copying lookup table to print a list of bit tags as zeroes and ones:

(((1)S:^)(!(0)S:^)):^(^!^!^^!^^^!^)^

Unlambda to Underload

The s, k, and i and v characters in Unlambda can all be translated directly into Underload. Also, the ` character can be translated, but it has to be moved to a postfix rather than prefix position, and .x can be translated for most values of x.

• s translates to ((:)~*(~)*a(~*(~^)*)*):

  sx`y`z` = xz`yz`` (postfix notation)
  sx`y`   = (:x~y~^)
  sx`     = ((:x~)~*(~^)*)
  s       = ((:)~*(~)*a(~*(~^)*)*)

• k translates to (a(!)~*)
• i translates to ()
• v translates to ((~!a(:^)*):^)
• ` translates to ~^
• .x translates to ((x)S)

These translations prove that Underload is Turing-complete, because it can be compiled into from the Turing-complete `sk Unlambda.

Underload minimization

While the Unlambda translation shows that Underload is Turing-complete, it uses all the commands in the language. We may ask whether only a subset suffices.

The commands :()^ are clearly necessary:

• Only () can be used without there already being elements on the stack.
• Without ^, the remaining program will always decrease in size, eventually halting.
• Without :, the size of the combined contents of the remaining program and the stack will always decrease in size, eventually halting, provided you count a's triply.

From there it gets more subtle: the program (::^):^ runs indefinitely, consuming unbounded memory.

Some of the remaining commands can be removed individually:

• S is unnecessary as long as we consider the final stack content to be part of the result.
• ~ is the only command whose effect can be written directly in terms of the others:

~ = a(!a)(!)(a*a*:*^!a*^):*^

• Removing just ! is relatively easy: Instead of deleting elements, keep all the "junk" on top of the stack, compacted with *. This can be done by transforming the program so that every command bypasses that top junk element:

{(x)}    = ({x})~
{xy...z} = {x}{y}...{z}
{x}      = (x)~a*^ for all x made up of ~:*S
{!}      = * or if you want nicely formatted junk, ~a*
{a}      = ~a(~)*~
{^}      = ~^
Call the whole program as (){P}.

• We can even combine the ideas for ~ and ! and remove both simultaneously, showing that :*()a^ is sufficient for Turing-completeness. Now the junk will not be cleanly separated, but may end up embedded inside stack elements. This method seems to use a lot of memory, at least if the interpreter does no sharing of sub-elements.

{}       = (j)
{xy}     = {x}a(*)**{y}
{~}      = aa((a(*)**((aa)(a(*)**))))*:*^a(*)****^a*^a*aa*(*:*^a(*)****^)*^(j)
{:}      = :(j)
{!}      =     [nothing]
{*}      = aa((a(*)**):a*)*:*^a(*)****^**(j)
{(x)}    = ({x})(j)
{a}      = a((j))*(j)
{^}      = ^
{(x)S}   = (x)S(j)
Call the whole program as (j){P}.
(j) denotes an arbitrary junk element.
Any (j)a(*)** arising from the expansion is redundant and can be removed.

We will now show that we don't need more than ~:()^ for Turing-completeness. The proof is in two parts: First we show how to implement an arbitrary Turing machine using ~:!()^. Then we show how to apply a program transformation to remove the use of !.

~:!()^ Turing machine

Let a Turing machine with m states numbered 0...m-1 and n symbols numbered 0...n-1 be given.

The following shows the basic layout of an Underload stack + program simulating the Turing machine at position i of a tape of length k at a point just before a lookup in the main rule table.

(^!x0)...(^!xi-1)(T):^!s^!xi^!xi+1^...!xk-1^

Symbols in the left part of the TM tape are represented as elements on the Underload stack, in the form (^!x), where the number of !'s equals the number of the symbol.

Then follows (T), the main rule table for the TM. This table is just about to be copied, and a lookup of the subtable for the current state s will be made. Then a lookup in that subtable for the current tape symbol x_i is made, running the action for that state and symbol.

Finally the right part of the TM tape is represented as commands in the remainder of the program. The command !x^ is ready to perform a subtable lookup for the symbol x, if and whenever the program reaches that point. We may also think of this as a way of representing the right part of the tape on a stack, namely the call stack of the Underload program.

The layout of the main rule table is as follows:

T = (Tm-1)(!Tm-2)...(!m-2T1)(!m-1T0)

Looking up a state s in the table is a matter of running the action of T to lay out the cases as elements of the stack, then performing s !'s to remove all cases above the correct one, and then running the subprogram for that case. The subprogram first takes care to remove any other cases remaining on the stack before performing its designated action. In this case the action is that of laying out cases for a subtable T_s:

Ts = (Tn-1s)(!Tn-2s)...(!n-2T1s)(!n-1T0s)

Finally each T^x_s is the designated action for a current state s and a current tape symbol x. There are several possibilities for this.

To put the symbol y in the current tape cell, then move left, and into state t:

~(:^!t^)~^^!y^

To put the symbol y in the current tape cell, then move right, and into state t:

(^!y)~:^!t^

Expanding the tape when necessary is achieved by replacing the current tape cell with more than one new cell. To replace it with two cells containing the symbols yz while moving left, staying on the y, staying on the z, or moving right, respectively:

~(:^!t^)~^^!y^!z^
:^!t^!y^!z^
(^!y)~:^!t^!z^
(^!y)~(^!z)~:^!t^

If we wish to allow S commands, it is also easy to modify actions to perform output. Halting is achieved by running off the right edge of the tape.

Removal of ! from ~:!()^ programs

Without the ! command available, the only command that can sometimes delete nontrivial stack elements cleanly is ^. Of course only some elements can be so deleted, e.g. (()()) can be deleted by three ^'s, while no element containing a non-command character or containing an infinite loop can be. Note that an element cannot be deletable without ! unless every sub-element of it also is.

We will describe a transformation which turns any ~:!()^ program into a !-less yet still deletable program that is capable of either running in a manner equivalent to the original, or of deleting itself cleanly, as appropriate, by providing the resulting program with an extra argument () or (~) on the stack to decide which action to perform.

If P is a program, we denote the transformed program by {P}. Then the required properties of the transformation are:

• (){P} behaves equivalently to the null program, i.e. {P} deletes the () from the stack with no other effect.
• ({A1})...({An})(~){P} behaves equivalently to (A1)...(An)P.

Our basic transformation rules are:

{}    = ()~()~^^^
{PQ}  = :({P})~(^())~(^(~))~^^()~^^{Q}
{~}   = ^
{:}   = ()~(:)~^(^)~^^
{!}   = ()~^^
{(P)} = ()~({P})~^^
{^}   = :^^

If we allow the command S as well, some forms of output can be supported (This list can probably be expanded with some parenthesized elements):

{(~)S} = S
{(:)S} = ()~(^)~(:)~()~^S^^
{(^)S} = ()~(^)~(:)~(:)~(^)~()~^S^(^)~^^^

For completeness we include a and *, which don't use ! in their transformations although they do use a and * themselves:

{a} = (^~)~^a(()~)~(~^^)**:()~^~()~()~^~^
{*} = ()~(^()(^)(^))~(^~a(:)~(~(^())~(^(~))~^^()~^^)**~*)~^^^

A Haskell program for helping with this transformation is available.

It is possible to take some shortcuts in the transformation if we know that an element will never need to be deleted, even as a sub-element of another element. This is especially simple if we know that the original element will also never be run with less than two elements on the stack: Prepending ^~ to the element is enough to get rid of the (~) on the stack. Note that it may still be necessary to transform some sub-elements.

The above transformation is rather verbose. Even using shortcuts, the first example program expanded to around 18 times the size.

:!()^ Minsky machine

A careful investigation of the :()^!~ Turing machine implementation above would show that the instruction ~ is only used whenever it is necessary to move information across the "tape head" formed by the main lookup table.

In the case when the Turing machine alphabet has only one symbol, it is possible to avoid the use of ~ by encoding the left part of the tape using copies of the element for the lookup table itself. It is also possible to have a special, left-most table to denote and detect the left end of the tape. Since the right part of the tape doesn't need ~ for its decoding, we can use two different symbols on that side to be able to denote the end there too.

With this, we have the necessary tools to implement a Turing-complete Minsky machine with two counters x and y.

((T)U)(T)x:^!s^^y!^ 

As before, T is a lookup table used for looking up the state s, giving as result another lookup table T_s, which is used to lookup either the action for the case y=0 (triggered by the !^ at the end of the program) or for the case y≠0 (triggered by ^.)

U is an alternative lookup table in the same format, used for lookup whenever x=0.

An action consists of up to four consecutive parts:

x adjustment	x-=n	no adjustment		x+=n
	!n			:n
Next state lookup	:^!s'
y adjustment	y--	no adjustment		y+=n
		^		^^n
End replacement	when y=0		when y≠0
	!^

Note that for technical reasons, whenever x or y is 0 it will effectively be incremented to 1 before the action is taken. This must be taken into account in writing such actions.

While it is possible to decrement x more than one step at once, the program will of course break if this would make x negative.

As before output may be added to actions. An empty action when y=0 halts the machine.

An example of this method is above.

Removal of ! from :!()^ programs

(Adapted from the #esoteric IRC channel. There is a Haskell program for doing the below transformations automatically.)

We would like to remove ! from the Minsky machine implementation in order to prove that :()^ is sufficient for Turing completeness. Like with the ~:!()^ case, we use a mechanism for turning a program into a corresponding one which can be run in either such a way as to emulate the original program, or in such a way as to delete itself. But without ~ it gets tricky to give the transformed program an argument to decide what to do.

However inspired by the :!()^ Minsky machine, we do a change of perspective: : can be seen as a command that gives the element on the top of the stack an extra argument, namely itself. Using this, if the top of the stack is of the form (^P), then we can run P either once or twice by using ^ or :^, respectively.

Consider a program P containing only : or ^, and not ending with : (P could be empty.) Now construct PL as follows: for every block of :'s followed by ^ in P, we let PL contain ()(^), for every single ^ we let PL contain (), in the reverse order of the corresponding P parts. (Example: PL = ()(^)()()()(^)()() , P = ^^:^^^::^.)

Then we can see that PLP is equivalent to the null program, while PLPP is equivalent to P.

(Incidentally whenever some LP is equivalent to the null program, P is equivalent to something of that :^ form. (L might not be just ()'s and (^)'s though.) This can be seen by reducing all parentheses in P away.)

Define {P} = PL()(^P). We then have that {P}^ is null and {P}:^ is equivalent to P. I.e. {P} is a conditionally runnable version of P, using ^ and :^ as deletion and running commands respectively.

Note that ^ and :^ are themselves of this left cancelable form. This means it will be convenient to use such conditionally runnable programs to control each other.

This is not sufficient to run every program conditionally however. For example we also need to handle parenthesized subprograms, which can never be left cancelable.

So, consider the more complicated case of a program P that may not be canceled solely by something on the left, but which can be canceled by something on the left and right combined. i.e. PLPPR is null for some PL and PR.

Also let PRLPR be null. (We could define PRL = PLP, but P may in many cases be much larger than necessary for this.) Define

{P} = PLPRL()(^PRP).

(This is an extension of the previous definition.) We get

{P}^  = PLPRL()(^PRP)^
      = PLPRLPRP
      = PLP.
{P}^PR = PLPPR = .
{P}:^ = PLPRLPRPPRP
      = PLPPRP
      = P.

Once again, {P}:^ is P, while on the other hand {P}^PR is null. Note that for this case the command to delete {P} is ^PR, which is dependent on P. This is a bit of a problem, as we need a common "API" for handling items that are put on the stack.

However ^PR is itself left cancelable (by PRL()), and so can be executed by a conditional program of the simple form. Define

{P}' = {P}{^PR}.

Since ^PR is left cancelable, we know that {^PR} is deleted by ^. This means that

{P}'^:^ = P.
{P}':^ is null.

This will be our "API" for running/deleting subprograms that end up inside parentheses, and that may be put on the stack. Note that once again, ^:^ and :^ are left cancelable.

This is still not enough to make every program deletable, e.g. the program (:^):^ cannot be cancelable no matter what you prepend and append, since it doesn't halt! However it turns out that after applying the transformation recursively on parenthesized subprograms, all the programs we need to handle split into parts that are cancelable. Assume that

P = QP1P2...Pn, with n≥1, QQR and PiLPiPiR being null.

The special case Q is for handling initial parenthesized subprograms a bit more efficiently. Q and P1 may be chosen empty if necessary. Now we define

{P}' = Q{P1}{:^P2}...{:^Pn}{^PnR...^P2R^P1RQR}.

Then this still obeys the same API as for a cancelable P.

(Each Pi block constructed by the Haskell program tends to be of a form similar to :^::^^:(...)...(...), with : and ^ (and sometimes S) first and parenthesized subprograms last.)

With the API settled, we can now transform individual commands to use it. Our transformation rules become:

<!> = ^:^.
<^> = ^^:^.
<:> = :.
<P1...Pn> = <P1>...<Pn>.
<(P)> = ({<P>}').
<(P1...Pn)S> = (P1)S...(Pn)S  where each Pi must be cancelable unless at top level.

We can also summarize the necessary cancelations in a table:

PL	P	PR	Conditions
			P is empty.
P2LP1L	P1P2	P2RP1R	Pi is cancelable, P1R or P2L is null.
()	^
()	S
()(^)	:n^
()(^)	:n	^
PL	(P)	^PR	P is cancelable.
	{P}	^PR	P is cancelable.
	{P}'	:^	P splits into cancelable parts.

A two-command basis for a pure concatenative language

A different minimization question is the following: How many commands does a pure concatenative language need in order to be Turing-complete, while only using concatenations of those commands?

Clearly one command is insufficient, because if any program doesn't halt then no longer program can either, because it has to start with the shorter one.

However, two commands are enough: We can use the commands M and ^, where

M = (~)(:)(^)(a)(*)(!!!!!!)

Then we have

! = M^
~ = M!!!!!^
(:) = M!!!!~!
(^) = M!!!~!~!
a = M!!~!~!~!^
* = M!~!~!~!~!^

and (:), (^), a and * allow us to build any program using the Underload :()^ commands that doesn't contain (). We can replace () by ((:)(:)(:)(:)(:)(:)!!!!!!) which also has no effect, where the in the exclamation marks are produced by M~!~!~!~!~!. If we drop one of the (:) strings the code is equivalent to (!) so we can target the :!()^ fragment directly.

"Lambda" terms and abstraction elimination

Programmers of Underload may wish to use named terms and subprograms for convenience. Similarly to how SKI calculus languages like Unlambda are usually programmed, we describe here a "lambda" syntax for extended Underload programs, and a method (abstraction elimination) for converting such syntax to Underload proper.

Our lambda syntax is as follows:

[(x1)(x2)...(xn)-A]

The meaning of this syntax is a program which pops n stack elements, and substitutes the programs/strings in them for the variables x1...xn in the subprogram A. xn is here the topmost of the popped elements.

Conversion rules

The following rules may be applied repeatedly until all lambda expressions have been removed from your program.

Note that the conversion naturally doesn't preserve the printed form of strings, although interpolating variables into them should work as you expect.

We use A, B and C to stand in for (possibly empty) subprograms which may contain variables. We use lower case x for a parameter variable, and X and Y for a subparameter list between a [ and the matching -.

[X-AB] = [X-A]B
 when B does not contain any of the variables from X.
[X-X] = 
 (Yes, the empty program.)
[X-((A))] = [X-(A)]a
[X-(BC)] = [X-(B)(C)]*
[XY-A] = [Y-[X-A]]
 (Note reversed order.)
[(x)-(A)(x)] = :[(x)-(A)]~
[X-(A)B] = [X-(A)X][X-B]
[(x)-] = !
[X-B] = [X-(B)]^

It is possible for these rules to loop. To avoid this you can always take the first one which applies, and not use a rule with empty B, C, X, or Y. Use of empty A is recommended.

The above rules are just a minimal sufficient set. There are of course many shortcuts that could be taken to get simpler resulting programs in many cases. E.g. the above rules don't get to any of ~: from their obvious corresponding lambda expressions. The following additional rules would work for these:

[(x)-(A)(x)] = (A)~          when x not in A.
[(x)-A(x)(x)] = [(x)-A(x)]:
[(x)-(x)A] = :[(x)-A]        Ok, so these two feel a bit contrived, choose any one.

If we extend the syntax a little to allow nested parameter lists, we can do deep pattern matching:

[(X)-A] = ^[X-A]

The rules above remain valid with nested parameter lists.

Rewriting semantics

The above command descriptions treat Underload similarly to an imperative, stack-based language like Forth. It is also possible to think of Underload as a language described by rewriting semantics (and I seem to recall ais523 telling that this was how the first implementation was made.) This semantics is confluent,^{[citation needed]} and so essentially makes Underload into an algebraic system. This viewpoint is implicitly used in much of the minimization section.

The rewriting rules hold perfectly only when applied at the top level of the program, i.e. not inside nested parentheses. The reason is that they do not preserve the output form of elements. As long as an element is not used as part of output, applying a rule inside it is fine.

Source	→	Result
(x)(y)~	→	(y)(x)
(x):	→	(x)(x)
(x)!	→
(x)(y)*	→	(xy)
(x)a	→	((x))
(x)^	→	x
(x)(y)S	→	(y)S(x)
(x)S(y)S	→	(xy)S

The rules for S are intended to gradually move output to the beginning of the program, thus preserving it but getting it out of the way.

Converting Underload to lambda calculus

It's possible to convert Underload programs to lambda calculus as in Iota and Jot's definitions on their original page. Unlike those languages, this translation uses a right-branching syntax. The generated programs convert functions acting on final stacks of the given program represented as a sequence of arguments to functions acting on initial stacks of the program.

Syntax	Semantics
F → e	^c.c
F → ( F1 ) F2	^c.[F2]c[F1]
F → ^ F	^cx.x([F]c)
F → : F	^cx.[F]cxx
F → ! F	^cx.[F]c
F → ~ F	^cxy.[F]cyx
F → a F	^cx.[F]c(^d.dx)
F → * F	^cxy.[F]c(^z.y(xz))

For example, here is a proof that a^ is αβη-equivalent to the empty program (note that admitting η-reduction is equivalent to assuming the stack never underflows)

[a^]
^cx.[^]c(^d.dx)
^cx.(^ey.y([]e))c(^d.dx)
^cx.(^ey.y((^f.f)e))c(^d.dx)
^cx.(^ey.ye)c(^d.dx)
^cx.(^y.yc)(^d.dx)
^cx.(^d.dx)c
^cx.cx
^c.c
[]

This is how :* reduces:

[:*]
^cx.[*]cxx
^cx.(^dyz.[]d(^w.y(zw)))cxx
^cx.(^dyz.(^e.e)d(^w.y(zw)))cxx
^cx.(^dyz.d(^w.y(zw)))cxx
^cx.(^yz.c(^w.y(zw)))xx
^cx.(^z.c(^w.x(zw)))x
^cx.c(^w.x(xw))

Applying this to the identity gives the usual Church numeral for 2, which is to be expected since :* is the Underload representation of 2.

External resources

• Underload at The Esoteric File Archive, which can be rendered as HTML via rawgit.com allowing you to run the Javascript interpreter on that page
• Try it online! interpreter
• Some Underload programs by User:Keymaker
• An Underload interpreter implemented in Redcode
• A compiler for Underload, compiling into Scala
• Joy, a more mainstream language based on similar principles
• Underload interpreter implemented in TeX
• Underload interpreter implemented in C

The information in the original version of this article was taken from the public-domain Underload specification (see The Esoteric File Archive links above).