# μ

Paradigm(s) Declarative User:Hakerh400 2021 Turing complete Implemented `.txt`

μ is an esolang invented by User:Hakerh400 in 2021. This language is named after the μ operator used in mathematics to denote minimization.

## Overview

This language operates on natural numbers (non-negative integers). A natural number is either zero, or a successor of a natural number.

Source code consists of functions. There is only one builtin function: `<=`. This function takes two arguments and returns `1` iff the first argument is less that or equal to the second argument, otherwise returns `0`.

Each function defined in the source code has one extra implicit argument. Such argument is the last argument of a function and such argument is not used explicitly when calling a function. When a function is called, the return value of the function is the smallest natural number such that, when that number is passed as the last argument, the function returns a non-zero value.

## Basic examples

### Constant zero

Here is how we define constant zero:

```zero a = a <= a
```

Here `a` is the implicit argument. Function zero actualy takes no arguments. The return value of `zero` is the smallest natural number `a` such that `a <= a` is a non-zero natural number. Since `0` is less than or equal to `0`, the result of `0 <= 0` is `1`, so `zero` always returns `0`.

### Constant one

Here is a function that always returns `1`:

```one a = (a <= a) <= a
```

If `a` is `0` then `a <= a` is `1`, but `1 <= a` is `0`. The smallest `a` for which `(a <= a) <= a` is non-zero is `1`, so the function `one` always returns `1`.

Here is a shorter example:

```one a = a
```

Basically, the smallest number that is truthy, which is `1`.

### Logical negation

We need a function that returns `1` if the argument is `0`, otherwise returns `0`. Since this function takes one argument, we need total of two formal arguments (because the second one is implicit):

```not a b = (a <= zero) <= b
```

If `a` is `0`, the smallest `b` for which the expression is non-zero is `1`. If `a` is non-zero, then the smallest `b` is `0`. So, this is a logical invertor. We can now use `0` as a falsy value and `1` as a truthy value.

### Logical implication

Logical implication from `a` to `b` is true if `a` is false or `b` is true. This function takes two arguments:

```(->) a b c = (a <= b) <= c
```

Checking all possible boolean combinations of `a` and `b`, it can be proved that this indeed represents the logical implication.

Note: we defined this function as an infix binary operator. We can use it in expressions like this: `a -> b`.

### Logical disjunction

```(||) a b c = (not a -> b) <= c
```

Note: prefix operators have higher precedence, so `not a -> b` is the same as `(not a) -> b`.

### Logical conjunction

```(&&) a b c = a <= (b <= c)
```

### Equality

```(==) a b c = ((a <= b) && (b <= a)) <= c
```

It returns `1` iff the two given natural numbers are the same. We achieved that by asserting that both `a <= b` and `b <= a`. In other words, we assert that the result `c` is the smallest number that is at least as truthy as `(a <= b) && (b <= a)`, which is exactly what we need.

### Not equals

```(/=) a b c = c == not (a == b)
```

### Less than (without being equal)

```(<) a b c = c == ((a <= b) && (a /= b))
```

It says: the first argument is less than or equal to the second argument, but they are not equal.

### Increment

```inc a b = a < b
```

The result is the smallest `b` such that `a < b`, which is exactly one more than `a`.

### Decrement

```dec a b = inc b == a
```

The result, when incremented, is equal to `a`.

Note: `dec 0` does not terminate, because there is no `b` such that `inc b == 0`.

```(+) a b c =
((b == zero) -> (c == a)) &&
((b /= zero) -> (c == inc (a + dec b)))
```

It says: if the second argument is `0`, the result is the first argument, otherwise the result is one more than the sum of the first argument and decremented second argument.

### Subtraction

```(-) a b c = (c + b) == a
```

Subtracting a larger number from a smaller number does not terminate.

### Multiplication

```(*) a b c =
((b == zero) -> (c == zero)) &&
((b /= zero) -> (c == (a + (a * dec b))))
```

### Division

```(/) a b c = (c * b) == a
```

Division by zero does not terminate (except if both operands are `0`, in which case the result is `0`). If the result would be a non-integer number, division also does not terminate.

## Interpreters

See the talk page.