# User:Hakerh400/Mink

Paradigm(s) Functional User:Hakerh400 2022 Turing complete WIP `.txt`

Mink is a work-in-progress esoteric programming language and theorem prover being invented by User:Hakerh400 during 2022 (and probably 2023).

### Overview

Mink is a functional programming language. There are no types. A value can be either Nil, a Pair, or Other.

Nil is a unique value. It contains no attributes. Any two Nils are identical.

A Pair has two elements. Both elements are values. Two Pairs are equal iff their corresponding elements are equal.

Other is a sort of value we can't reason about. We don't know what it contains or how it's structured. It cannot be equal to Nil or a Pair.

A value does not need to be finite. For example, we can have a Pair that contains itself as both elements. It is a valid value.

### Syntax

Syntax may change in the future. For now, Nil is represented as `0`, Pair is `(a, b)` and Other is `@x` where `x` is some unique identifier.

Natural number `0` represents Nil and for any natural number ${\displaystyle n}$, if ${\displaystyle n}$ represents value `x`, then ${\displaystyle n+1}$ represents value `(0, x)`.

### Reduction rules

Each value can be called like a function. We represent call as two values separated by a space. For example `a b` represents calling value `a` with argument `b`.

When Other is called, the result is undefined (there are no explicit reduction rules). In some cases we can figure out what the result is, but in most cases we cannot.

When a Pair is called, it passes it's elements to the argument. For example, `(a, b) f` reduces to `f a b`.

Nil takes three arguments. If the first argument is Nil, it returns the second argument. If the first argument is a Pair, it returns the third argument. If the first argument is Other, the result is some Other (it may or may not be equal to the first argument).

### Functions

A function is also a value. Each function is internally represented as a combination of Nils, Pairs and Others. Functions can be defined by explicit reduction rules. This is an example:

```fst_arg a b = a
```

This function has name `fst_arg`. It takes two arguments and returns the first one. We can't always reason about the internal representation of a function, but the definition gives us the explicit reduction rules for that function. Whenever we see `fst_arg a b` for any values `a` and `b`, we can reduce it to `a`.

Partial function application is also possible.

Function equality is not extensional. It means that two functions may not be equal even if they agree on all inputs. For example:

```func1 a = a
func2 a = a
```

We can't prove that `func1` is equal to `func2`, although we can prove that for any fixed `a`, the results are equal. That's because the compiler may choose different internal representations for those two functions.

On the other hand, `x` and `y` are equal in the following example:

```x = 5
y = 5
```

because they do not take any arguments, so we know they are both equal to `(0, (0, (0, (0, (0, 0)))))` - the expanded representation of the natural number `5`.

### Propositions

A value is considered true iff it reduces to nil in a finite number of steps by applying reduction rules, or false otherwise. A proposition is an assertion that a value is true.

### Example

We define the following functions/constants:

```T = 0
F = 1
nil = 0
ite = nil
id x = x
fst_arg x y = x
snd_arg x y = y
const = fst_arg
dot f g x = f (g x)
flip f x y = f y x
fix f = f (fix f)
K = const
S a b c = a c (b c)
I = id
fst a = a fst_arg
snd a = a snd_arg
not a = ite a F T
and a b = ite a b F
or a b = ite a T b
imp a b = or (not a) b
iff a b = and (imp a b) (imp b a)
Any a = T
Nil a = ite a T F
Pair a = ite a F T
Term a = or (Nil a) (Pair a)
Prop a = or (Nil a) (and (Pair a) (and (Nil (fst a)) (Nil (snd a))))
Tree a = or (Nil a) (and (Pair a) (and (Tree (fst a)) (Tree (snd a))))
Nat a = or (Nil a) (and (Pair a) (and (Nil (fst a)) (Nat (snd a))))
```

`T` represents true and `F` represents false (because `T` reduces to Nil and `F` doesn't). We call `T` and `F` propositions. After that, we define `nil` to be `0` for convenience.

Then we define `ite`, which stands for if-then-else. It is equal to `nil`. If you think about it, `nil` takes three arguments and returns the second or the third argument based on the value of the first argument (except if it's Other). That's what if-then-else does. Note that `ite = nil` is a stronger statement than `ite a b c = nil a b c`, because of how function extensionality works.

Definitions from `id` to `I` should be obvious and don't need explanation. Then we have `fst`, which returns the first element of a pair. It takes argument `a` (which we asume is a pair) and calls it with `fst_arg` as the argument. If `a` is a pair, for example `(b, c)`, then `(b, c) fst_arg` reduces to `fst_arg b c`, which reduces to `b`. Similar applies to `snd`. Both `fst` and `snd` expect the argument to be a pair. If it is not a pair, then it may be hard (or impossible) to prove what the result would be.

Then we have some logic functions (from `not` to `iff`). After that, we have "types". A type is a predicate (a function that returns a proposition). Type `Any` always returns true (it is the most general type). Type `Nil` returns true iff the argument is `nil`. Type `Term` encompasses the nil and all pairs. Type `Prop` encompasses only `T` and `F` (`0` and `1`). Type `Tree` encompasses all finite trees (Nil is a finite tree and whenever `a` and `b` are finite trees, the pair `(a, b)` is also a finite tree for any values `a` and `b`). Type `Nat` encompasses all natural numbers.

### Theorems

A theorem has the following structure:

```name arg1 arg2 ... argn : asm1 → asm2 → ... → asmk → conclusion
proof
```

Identifier `name` is the name of the theorem. Identifiers `arg1 arg2 ... argn` are theorem parameters (universally quantified values). Expressions `asm1 asm2 ... asmk` are assumptions that each of those expressions is true (reduces to nil in a finite number of steps). Expression `conclusion` is the goal that has to be proved using the assumptions. The `proof` proves the theorem using assumptions and tactics.

### Tactics

There are foundational and derived tactics. Foundational tactics represent the fundamental inference rules axiomatized by the kernel (the core of the theorem prover). Derived tactics are built on top of the foundational tactics via metaprogramming.

We haven't decided yet what tactics to have. The idea is to have some basic tactics about equality and rewriting. We also need induction.

### Induction

How is the induction supposed to work? We haven't figured out yet. We can't perform induction on values directly, because a value can be anything, it doesn't even need to be structurally finite. The only thing we can perform induction on are assumptions. Consider this theorem:

```tree_of_nat a : Nat a → Tree a
```

It asserts that if value `a` is a natural number, then it is also a finite tree. That's true, because of how natural numbers are represented. The assumption `Nat a` asserts that the expression `Nat a` terminates after a finite number of steps and returns `T`. We can somehow perform induction on it and reduce the proof obligations to

```Tree 0
∀ n, Tree n → Tree (0, n)
```

The first can be proved trivially by applying reduction rules. The second can be proved by unfolding `Tree (0, n)` and simplifying logical operators.

### Implementation

We played with this idea and implemented it in Haskell (repository), but it's far from finished.