Amicus

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

The motivation why Amicus was supposed to be 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 that language is correct and understandible, he first defined a Turing-equivalent language, and then an extension that turns that language to its hyperarithmetic version.

Definition

The basic data type of Amicus 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:d>…>>>) = 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: r>) = E(h, r)

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

Writing Amicus programs

There is a mechanical method to translate multivariate lambda calculus programs to Amicus. 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, and v will abbreviate the translated parameter tuple <v1, …, vm> = <T(x1), …, T(xm)>.

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 f = (\(x1, …, xm) -> e) to an Amicus program, such that E(T(f), <T(x1), …, T(xm)>) = T(f(x1, …, xm)) = T(e). With the above conventions, we abbreviate that like: for any weak normal form lambda expression f = (\x -> e), we will define T(f) such that E(T(f), v) = T(f(x)) = T(e). Amicus 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 Amicus 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(\x -> 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>, T(\x -> q), 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.

To see why this works, first note that since every Amicus value is a finite list, Rule 6 could equivalently have been written as the following: E(<6>, <f, r1, …, rn'>) = E(f, <r1, …, rn'>) for every natural n'.

Now recursively: E(T(\x -> q), v) = T(q) and E(T(\x -> p1), v) = T(p1) and … E(T(\x -> pn), v) = T(pn). Also, E(T(q), <T(p1), …, T(pn)>) = T(q(p1, …, pn)).

Then, applying Rule 6 with n' = n+1, r1 = T(q), r2 = T(p1), …, rn' = T(pn), we get: E(<6>, <T(q), T(p1), …, T(pn)>) = E(T(q), <T(p1), …, T(pn)>).

Next, we apply Rule 5, and then use the previous equalities: E(<5, <6>, T(\x -> q), T(\x -> p1), …, T(\x -> pn)>, v) = E(<6>, <E(T(\x -> q), v), <E(T(\x -> p1), v), …, E(T(\x -> pn), v)>) = E(<6>, <T(q), T(p1), …, T(pn)>) = E(T(q), <T(p1), …, T(pn)>) = T(q(p1, …, pn)).

Upvalue rule

T(\x -> (\(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 natural numbers, in such a way that the numbers are represented by the native Amicus numbers. For integers, you must use rules 2 and 4.

Integer rule

T(k) = k.

Equality rule

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

Succ rule

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

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

Zero literal rule

T(\x -> 0) = <5, <0>>.

K rule

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

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

This rule is recommended when c is an integer literal, but is still always optional. If c is an integer literal, then you can rewrite (\x -> c) = (\x -> Succ(…Succ(0,)…,)) where succ is the above defined function and it is nested c times. 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 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 Amicus. This relies on all numbered rules, and does not rely on the representation of lists as numbers; but if you want to completely forbid Rule 1, then you have to rely on the representation of the empty list as 0 in the zero literal rule.

Implementing Amicus

Should you wish to implement Amicus, 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(<<>: <>>) = <<<>: <>>: <>>;
• succ(<<>: <e: m>>) = <succ(e): succ(m)>;
• 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 Amicus program itself cannot use the above method to increment numbers, because it cannot get the tail of a list without using the increment primitive.

Amicus Severus

David gives a partial implementation of Amicus 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 this restricted language Amicus 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.

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 Amicus, which all works just the same in Amicus Severus.

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

A more formal definition

For a formal definition of Amicus Severus, we have to forget the definition of Amicus.

A value in Amicus Severus is either a natural number of unbounded size, or a finite size list of values. Lists are written as <x1, …, xn> where n is a natural number, and x1, … xn are values. (You could think of Amicus Severus values as binary trees with a natural number in each leaf. A list can contain numbers or lists, or the two mixed. Amicus Severus cannot create circular or infinite lists.)

Amicus Severus programs are list values whose head is an opcode number. Amicus Severus takes such a program, and a single input argument which is a value (number or list), and gives a value as the result. Evaluation is defined by the following recursive definition, where E(p, x) = y means that the program p on the input x 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>, <x1, …, xn>) = xn, provided 0 < n

Rule 4.

E(<4>, <m, n, u, v>>) = (if m == n then u else v) provided m, n are both natural numbers

Rule 5.

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

Rule 6.

E(<6>, <h, r1, …, rn>) = E(h, <r1, …, rn>)

Rules 5 and 6 apply for every natural number n.

Interpreter

The following example interpreter in scheme is by David Madore from the blog entry Qu'est-ce qu'une machine hyperarithmétique ? .

  (define (ev prgm args) (if (not (list? prgm)) (error "prgm is not a list")) (let ((inst (car prgm))) (case inst ((0) args) ((1) (cadr prgm)) ((2) (+ (car args) 1)) ((3) (list-ref args (- (cadr prgm) 1))) ((4) (if (= (car args) (cadr args)) (caddr args) (cadddr args))) ((5) (let ((vals (map (lambda (p) (ev p args)) (cddr prgm)))) (ev (cadr prgm) vals))) ((6) (ev (car args) (cdr args))) (else (error "unknown instruction")))))

This defines a scheme function ev which takes two arguments, an Amicus Severus program, and an argument for the program, and returns the result of running the program. Amicus Severus numbers are represented as scheme numbers, and Amicus Severus lists as scheme lists in the natural way. This interpreter sometimes accepts invalid programs or arguments, in which some lists involved have extra elements, but this probably does not impact the integrity of Amicus Severus.

Amycus

The esoteric language Amycus was created from Amicus two days after its publication, when User:b_jonas tried to understand and document it on the Esolang wiki, but documented a very different language instead. The language Amycus Severus was then created from #Amicus Severus by consistently following the same misunderstanding. While writing the article for Amycus, I kept typoing its name as “Amicus”. Thus, I eventually decided to use the name Amicus for David's original language.