Amycus

Amycus is a simple Turing-complete functional programming language created by a misunderstanding from a language Amicus defined by David Madore in his 2015-11-16 blog article “Qu'est-ce qu'une machine hyperarithmétique ?”. Just like David's older language Unlambda or Backus's FP language, Amycus has no variables, yet lambda calculus style code with variables can be translated to Amycus easily by abstraction elimination, because the necessary combinators for composition are provided.

The motivation why this language came to being is that David wanted to give a precise definition for a larger computability class called “hyperarithmetic function” by defining the programming language Hyperamicus. To ensure that the definition of Hyperamicus is correct and understandible, he first defined a Turing-equivalent language Amicus, and then an extension that turns that language to Hyperamicus.

Definition

The basic data type of Amycus is natural numbers of unbounded size, but these numbers are usually treated as representing recursive lists in the Lisp sense. The empty list <> is represented by the number 0, the list <a: d> with head a and tail d is represented as the number 2**a * (2 * d + 1), and in general a finite list <v1, v2, …, vk> is represented as <v1: <v2: <… <vk, <>>…>>>, or 2**v1 + 2**(v1+v2+1) + … + 2**(v1+v2+…+vk+(k-1)). This construction makes every natural number a list.

Programs are represented as a number (list), operate on a single input argument which is also a number (list), and give a single number (list) as the result. There is no IO or other side effects. Evaluation is defined by the following recursive definition, where E(p, v) = y means that the program p on the input v evaluates to the value y.

Rule 0.

E(<0>, v) = v

Rule 1.

E(<1, c>, v) = c

Rule 2.

E(<2>, <n: r>) = 1 + n

Rule 3.

E(<3, n>, <v1: <v2: <…, <vn: r>…>>>) = vn, provided 0 < n

Rule 4.

E(<4>, <m, n, u, v>>) = (if m == n then u else v)

Rule 5.

E(<5, f, g1, …, gn>, v) = E(f, <E(g1, v), …, E(gn, v)>)

Rule 6.

E(<6>, <h, v>) = E(h, v)

Rule 5 is valid for any natural number n. As a special case, E(<5, q>) = E(q, <>) = E(q, 0).

Origins

Amycus was born from a misunderstanding. The original (nameless) language had a different rule 6:

Original rule 6.

E(<6>, <h: r>) = E(h, r)

The one character difference in the rule significantly changes the language, and by the time David pointed out User:B_jonas's mistake, it was too late to undo. In particular, David's language is more consistent and easier to program than Amycus, but leads to fewer interesting crazy variants.

David didn't give a name for this language, so User:B_jonas tried to give the name “Amycus” as a placeholder before he knew it was a different language. The original language is now called “Amicus”.

Writing Amycus programs

There is a mechanical method to translate multivariate lambda calculus programs to Amycus. Here, multivariate lambda calculus means that lambda expressions abstract over a list of variables, and the expression inside can contain each of those variables.

In all the following description, x1, …, xm, y1, …, yn, z1, …, zr stand for individual symbolic variables of the lambda calculus; and x will abbreviate the parameter tuple (x1, …, xm) for brevity.

Abstraction elimination

The method of translation relies on eliminating abstractions, similar to programming Unlambda or S-K combinator calculus.

We will recursively define a function T that translates any weak normal form lambda expression combinator p = (\(x1, …, xm) -> e) to an Amycus program, such that E(T(p), <T(x1), …, T(xm)>) = T(p(x1, …, xm)). Amycus executes such lambda expressions in a strict way, and if the lambda expression never halts in a strict lambda calculus interpreter (similar to Unlambda), then Amycus will not halt on the corresponding program and input either.

K rule

T(\x -> c) = <1, T(c)>,

where c is a constant, that is, it has no free variables.

This rule is optional, you can always use one of the other rules instead, but it can simplify a lot.

I rule

T(\(x1, …, xm) -> xk) = <3, k>.

B rule

T(\x -> q(p1, …, pn)) = <5, T(q), T(\x -> p1), …, T(\x -> pn)>,

provided that q is a constant lambda expression that has none of the variables x1, …, xm;

and p1, …, pn are arbitrary expressions that may contain some of those variables.

This rule is optional, because you can always use the S rule instead, but it can simplify a lot, and help understanding.

S rule

T(\x -> q(p1, …, pn)) = <5, <6>, <5, <0>, T(\x -> q), <5, <0>, T(\x -> p1), …, T(\x -> pn)>>>,

where not only p1, …, pn but also q are expressions that may contain some of the variables x1, …, xm.

The reason why this works is that t = E(<5, <0>, T(\x -> q), <5, <0>, T(\x -> p1), …, T(\x -> pn)>>, <T(x1), …, T(xm)>) = <T(q), <T(x1), …, T(xm)>>, and then E(<6>, <t, <T(x1), …, T(xm)>>) = E(t, <T(x1), …, T(xm)>) =

Upvalue rule

T(\(x1, …, xm) -> (\(y1, …, yn) -> q)) = <5, <0>, <1, T(p)>, <3, 1>, …, <3, m>, <1, <3, 1>>, …, <1, <3, n>>>,

where p = (\(x1, …, xm, y1, …, yn) -> q).

Here q is an arbitrary expression that can contain some of the variables x1, …, xm, y1, …, yn.

Note that p is a function where all variables x1, …, xm, y1, …, yn are bound, so it does not depend on x1, …, xm.

The reason why this works is that (\(x1, …, xm) -> \(y1, …, yn) -> q) = (\(x1', …, xm') -> \(y1, …, yn) -> p(x1', …, xm', y1, …, yn));

then T(\(y1, …, yn) -> p(x1', …, xm', y1, …, yn)) = <5, T(p), <1, T(x1')>, …, <1, T(xm')>, <3, 1>, …, <3, n>>.

None of this so far depends on the representation of lists as numbers, nor on rules 2 or 4.

Integers and lists

It is then possible to expand this translation from simple lambda calculus to a larger calculus that can handle lists of known length and natural numbers, in such a way that the numbers and lists are represented by the native numbers and lists of Amycus. For integers, you must use rules 2 and 4. If you chose to depend on the representation of lists as integers, you can use equality for lists too, meaning recursive equality.

List rule

T(\x -> <p1, …, pn>) = <5, <0>, T(\x -> p1), …, T(\x -> pn)>,

where p1, …, pn are arbitrary expressions that may depend on x.

Integer literal rule

T(k) = k.

Equality rule

T(\(k, l, c, d) -> if k == l then c else d) = <4>.

Nth rule

T(\(x1, …, xm) -> yj where <y1, …, yn> = xk) = <5, <6>, <5, <0>, <1, <3, j>>, <3, k>>>.

Or so I hope. Someone should check this rule.

Succ rule

T(\(k,) -> k + 1) = <2>,

where (k,) is a one-element list of the number k.

K rule

T(\x -> c) = <1, T(c)>,

where c is a constant, that is, it has no free variables.

This rule is now mandatory if c is an integer literal, but is optional in other cases. If one of the above arithmetic primitive functions (equality or successor) is used as the head of a function call, you can use the B rule instead. If an arithmetic primitive is used anywhere else, you either have to use this rule, or else eta-unreduce the lambda expression and then use rule B.

This proves that we can handle arbitrary natural numbers as input and output in Amycus. This relies on all seven numbered rules, but still does not rely on the representation of lists as numbers.

Abstraction elimination from the inside

As they are described above, you have to apply the translation rules for the outermost expression first, because they work only for expressions without free variables. Inner expressions may contain free variables, but the upvalue rule makes sure to bind these variables before attempting to recurse into the translation T.

This is possible because the translation rules work for lambdas with any number of parameter variables, which the Amycus language makes easy. This possibility is what makes programming Amycus easier than programming Unlambda, and somewhat similar to programming Backus's FP language. When translating a nested lambda expression, the upvalue rule needs to collect the variables bound by all outside lambdas together to a single parameter list.

There is, however, a generalized way to do the translation that lets you translate from inside out if you wish. This is more difficult to describe. Here, we generalize the translation to handle lambda expressions that may contain free variables, in which case the translation of these free variables will occur as a symbolic expression in the result, possibly nested deeply inside tuples. In this case, you need not use the upvalue rule to translate nested lambdas form the outside, but you may start by translate the inner lambda first.

For this, T is generalized to a function the translates any weak normal form lambda calculus expression to a nested list that may contain the translations of free variables of that expression as a free symbolic variable. More precisely, if e is a lambda calculus expression in weak normal form which may contain some free variables z1, …, zr, (thus e may be a lambda abstraction, an integer literal, tuple, or a free variable), then T(e) is a recursive list whose leafs may contain integer literals and the symbolic variables T(z1), …, T(zr), but not other variables. In particular, T(e) will not contain lambdas, bound variables, and would become an Amycus value if you substituted the symbolic variables T(z1), …, T(zr) with Amycus values.

K rule

T(\(x1, …, xm) -> c) = <1, T(c)>,

where c is an expression that may contain free variables, namely some of z1, …, zr, but not any of the variables x1, …, xm.

This is the rule you must use if c is a free variable, or an integer literal. It is optional in other cases.

Lambda rule

T(\(x1, …, xm) -> (\(y1, …, yn) -> q)) = T(\(x1, …, xm) -> T(\(y1, …, yn) -> q)),

Here is what the expression means. First evaluate t = T(\(y1, …, yn) -> q) to a nested list that may contain some of the symbolic variables T(x1), …, T(xm) in its leafs. As a result, T(\(x1, …, xm) -> t) can be computed using purely by recursively applying the List rule, the I rule (on the variables x1, …, xn), and the K rule.

The Upvalue rule, as given above, is actually derived by first applying the transformation (\(x1, …, xm) -> \(y1, …, yn) -> q) = (\(x1', …, xm') -> \(y1, …, yn) -> p(x1', …, xm', y1, …, yn)), where p is defined as in that rule, and then applying the Lambda rule to (\(y1, …, yn) -> p(x1', …, xm', y1, …, yn)) and the B rule to the whole expression.

Other rules

The I, B, S, List, Nth, Equality, Integer, Succ rules apply with an unchanged description, but some of the expressions q, p1, …, pn mentioned in them may now also contain free variables. You may still apply the Upvalue rule, but it is now entirely optional, because the Lambda rule can now take its place.

This variant of translation is more similar to how you usually do abstraction elimination in Unlambda.

Restricted variants

The really interesting thing about Amycus is the number of variants you can get by restricting its rules. This results in languages with various different properties and power, and so is worth to study.

Amycus Severus

David gives a partial implementation of the language Amycus was supposed to be in the blog post. This interprets the subset of the language where you can't convert numbers to lists or lists to numbers. I call that language “Amicus Severus”. If you transform this language to use the misunderstood rule 6, I get a language that I call “Amycus Severus”.

This means that lists and numbers are now separate data types, so the equivalence <a: d> = 2**a * (2 * d + 1) no longer stands. The program (and each subprogram evaluated during it) must be a list but its head must be a number. Rule 2 and rule 4 can increment or compare only numbers, rule 3 can only index into a list, rule 5 needs the list of subfunctions given as a list and passes a list to the first function. A more formal definition is given in the Amycus Severus article.

This subset of the language is already Turing-equivalent, and can read and write any number as an input. You can see this exactly the same way as the above proof, by translating lambda expressions with arithmetic to Amycus, which all works just the same in Amycus Severus.

However, an Amycus Severus program can handle and create lists of only bounded size, and even then only in limited ways.

Omitting rules 2 and 4

If you omit rule 2 and 4 of Amycus, keeping only rules 0, 1, 3, 5, 6, the restricted language is still Turing-complete, but requires special format of input and output arguments, because it cannot manipulate arbitrary numbers. This is true even if you start from Amycus Severus.

You can prove Turing-completeness by observing that the above translation rules from lambda calculus still apply.

With this restriction, the language can manipulate lists if it knows their length at compile time, by building a list of fixed length or accessing an element of a list of fixed length. In particular, the List rule and the Nth rule still apply. The language can also represent numeric symbols from a compile time fixed finite set of symbols s0, …, sN in the form where the symbol sn is represented by Sn = T(\(x0, …, xN) -> xn) = <3, n + 1>. This is enough to represent any ordered tree of compile-time bounded degree (recursive lists where each list has compile-time bounded length) as tagged lists. That is, you transform the list [c1, …, cn] to the tagged list <Sn, <c1, …, cn>>. An Amycus program can read the arity n of such a list, and then extract the elements of the list.

More formally, use the following transformation rules (after finding and fixing all typos in them).

New list literal rule

T([c1, …, cn]) = <Sn, <c1, …, cn>>

where Sn = <3, n + 1>.

Here, c1, …, cn are arbitrary nested square bracketed lists.

This rule is mandatory for translating each the input argument xn.

The rule can optionally be used to translate constant lists appearing inside the program, but you can use the following rule recursively instead.

As a special case, T([]) = <<3, 0>>.

Note that Sn = <3, n + 1> = T(\(x0, …, xN) -> xn) is effectively the translation of sn.

New list rule

T(\x -> [y1, …, yn]) = <5, <0>, <1, <3, n + 1>>, T(\x -> y1), …, T(\x -> y1)>.

Here, n is a compile time constant, and y1, …, yn are arbitrary expressions that may contain x1, …, xm as free variables. As such, any yk may have a lambda abstraction or a bracketed list or even an application at top level.

As a special case, T(\x -> []) = <5, <0>, <1, <3, 1>>> is a valid translation. However, T(\x -> []) = <1, <<3, 1>>> can be used instead as a shortcut rule.

New match rule

T(\x -> case q' of { [] -> p0', …, [y1, …, yN] -> pN' }) = <5, <6>, <5, <0>, <3, 1>, <5, <0>, v0, …, vN>>>

where vn = <5, <0>, <1, T(tn)>, <3, 1>, …, <3, m>, <1, <3, 1>>, …, <1, <3, n>>>,

tn = (\(x1, …, xm, y1, …, yn) -> pn').

for each n in 0, …, N.

Here, q' is an expression that may contain some of x1, …, xm as free variables,

and each pn' is an expression that may contain some of x1, …, xm, y1, …, yn as free variables.

Note that tn = (\(x1, …, xm, y1, …, yn) -> pn') is a constant lambda expression that contains no free variables and so can be translated recursively.

To derive this rule, first use the transformation (\x -> case q' of { …, [y1, …, yn] -> pn', … }) = (\x -> q0'(…, (\(y1, … yn) -> pn'), …) where <q0': qr'> = q'), then translate the right hand side by using the S rule

with N parameters,

with q = (q0' where <q0': qr'> = q') used as the head,

so q is translated by the Nth rule as T(\x -> q) = T(\x -> q0' where <q0': qr'> = q') = <3, 1>,

and each argument expression pn is computed as pn = (\(y1, … yn) -> pn')

and (\x -> pn) is translated by the upvalue rule as T(\x -> pn) = T(x -> \(y1, … yn) -> pn') = <5, <0>, <1, T(tn)>, <3, 1>, …, <3, m>, <1, <3, 1>>, …, <1, <3, n>>>.

Other rules

The K, I, B, S, Upvalue rules still apply normally.

If you use these rules, then E(T(p), <T(x1), …, T(xm)>) = T(p(x1, …, xm)), where E evaluates Amycus Severus without rule 2 or 4.

This translation also has an inside-out variant, where you generalize the translation so the translated expression can contain symbolic free variables, and may use the Lambda rule.

As a conclusion, an Amycus Severus without rule 2 and 4 program can represent any computable function from ordered trees of compile-time bounded degree to ordered trees of compile-time bounded degree, by representing these trees the above way. In particular, Amycus Severus without rule 2 and 4 is still Turing-complete.

If you permit rule 4 but forbid rule 2, starting from either Amycus or Amycus Severus, the situation is very similar, but you may optionally use a different representation of tags, with Sn = n, which would simplify some of the translation rules a bit.

However, if you do not know anything about an input number (list) in advance, then the only way to access it in Amycus without undefined behavior is to start incrementing numbers with rule 2 and compare each one with the number using rule 4, eventually finding the number it is equal to. Rules 4 and 2 let an Amycus program read and write any natural number and thus any list. Thus, Amycus without rule 2 cannot represent every computable function from natural numbers to natural numbers as an Amycus program. In fact, it cannot even represent every computable program that takes a natural number as an input with either a fixed value as the result or an infinite loop.

TODO earlier notes

I should to clean up this section later by expanding above. I will have write about the consequences of omitting rule 0, omitting rule 0 and 2, omitting rule 1, and omitting other rules. David suggests that rule 0 might not be necessary. This is true in a sense, which I shall describe later.

User:B_jonas currently believes the following, but this will require more thought.

• Amycus without rules 1, 2, 4 is still Turing-complete and can be programmed reasonably easily in a similar way to Amycus without rules 2, 4.
• Amycus without rule 0 is still Turing-complete but is much more limited than Amycus. Namely it can't directly bulid tree structures, is at least as powerful as a machine with unbounded integer registers (Fractran), and at most as powerful as a machine with a stack of integer registers. The same is true for Amycus Severus without rule 0.
• Amycus without rules 0, 2 or without rules 0, 4 is no longer Turing-complete, and is at most primitive recursive. It might be able to run any primitive recursive program, but it's not clear to me whether the translation can be done in a polynomial time, or requires more time, in which case everything can be done in the translation. The same is true if you start from Amycus Severus.
• Amycus without rule 5, or without rule 6 can't do anything interesting. Amycus without rule 3 is probably like that too.
• I don't know anything about Amycus without rules 0, 1 yet.
• I don't know anything about Amycus Severus without rule 0, or without rules 0, 1 yet.

Implementing

Should you wish to implement Amycus, it might be the easiest to store every value as a list, rather than a number. Every number is also a list, equality of two numbers can be computed as recursive comparison of two lists, and incrementing a number can also be computed on lists in a not too complicated way. Indeed, 1 + x = succ(x) can be computed recrusively with the following rules.

• succ(<>) = <<>: <>>;
• succ(<<>: n>) = <succ(e): m> where <e: m> = succ(n);
• succ(<e@<p: q>: m>) = <<>: <pred(e): m>>;
• pred(<>) = undefined;
• pred(<<>: <>>) = <>;
• pred(<<>: <e, m>>) = <succ(e): m>;
• pred(<e@<p: q>: m>) = <<>: pred(<pred(e): m>)>;

However, an Amycus program itself cannot use the above method to increment numbers, because it cannot get the tail of a list without using the increment primitive.