Μ

μ 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.
=== Addition ===
 (+) 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.
Category:Languages
Category:Turing complete
Category:2021
Category:Implemented