User:Hakerh400/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 , if represents value x
, then 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.