User:Hakerh400/Mink

Mink

Paradigm(s)	Functional
Designed by	User:Hakerh400
Appeared in	2022
Computational class	Turing complete
Major implementations	WIP
File extension(s)	.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 $n$, if $n$ represents value x, then $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.