|Computational class||Turing complete|
Mink is a work-in-progress esoteric programming language and theorem prover being invented by User:Hakerh400 during 2022 (and probably 2023).
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 may change in the future. For now, Nil is represented as
0, Pair is
(a, b) and Other is
x is some unique identifier.
0 represents Nil and for any natural number , if represents value
x, then represents value
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
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).
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
b, we can reduce it to
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,
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
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.
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
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.
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 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
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
Term encompasses the nil and all pairs. Type
Prop encompasses only
Tree encompasses all finite trees (Nil is a finite tree and whenever
b are finite trees, the pair
(a, b) is also a finite tree for any values
Nat encompasses all natural numbers.
A theorem has the following structure:
name arg1 arg2 ... argn : asm1 → asm2 → ... → asmk → conclusion proof
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.
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.
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.
We played with this idea and implemented it in Haskell (repository), but it's far from finished.