SKM Calculus
| Paradigm(s) | Functional |
|---|---|
| Designed by | User:Hakerh400 |
| Appeared in | 2022 |
| Computational class | Turing complete |
| Major implementations | Implemented |
| File extension(s) | .txt |
SKM Calculus is an esoteric computational model invented by User:Hakerh400 in 2022.
Overview
SKM calculus is very similar to SKI calculus, but has additional combinator M, which cannot be implemented in SKI.
Combinators
There are three combinators: K, S and M. Two combinators are equal iff they have the same name (so, for example, any two K are equal, but K is not equal to S).
Expression
An SKM expression is either a combinator, or an application of two expressions. All expressions are finite. Application of expressions a and b is represented as a b. Application is left-associative (for example, a b c is interpreted as (a b) c, and not a (b c)). In application a b, expression a is called function and expression b is called argument.
Reduction step
For any expressions a and b, expression K a b reduces to a in a single step.
For any expressions a, b and c, expression S a b c reduces to a c (b c) in a single step.
For any expression a, expression M a reduces to a iff a reduces either to K or S.
Reduction
Expression a reduces to expression b iff a can be transformed to b by applying finitely many reduction steps.
However, unlike in SKI, reduction is more restrictive. For example, in SKI, if a reduces to b, then f a reduces to f b for any SKI expressions a, b and f. That's not the case in SKM. We can't reduce argument before we reduce the function (except if the function is M, because that is allowed by the third reduction step rule). For example, K (K K K) does not reduce any further, because no reduction steps can be applied to the main expression, despite the fact that K K K reduces to K. On the other hand, M (K K K) indeed reduces to K (first reduces to M K and then to K).
We say "reduces to" instead of "can be reduced to", because there is only one way to reduce expressions. If a reduces to b1 in n1 steps, and a reduces to b2 in n2 steps, then n1 = n2 implies b1 = b2 (here n1 and n2 are natural numbers, while b1 = b2 represents syntactical equality).
Reduction is syntactically represented by a ==> b (expression a reduces to expression b).
Motive
The idea behind the M combinator is to allow implementing safe data structures without having data types. In SKI (and untyped lambda calculus), we can't have a data structure that we can safely inspect. For example, in SKI we can implement natural numbers using Church numerals, but we can't reliably tell whether a number is zero or a successor, because the only way to inspect a value (expression) is to call it and hope the result will be something meaningful. However, we may have any value, even a value that doesn't represent a valid Church numeral and which returns some junk when called.
The point of the M combinator is to have strict pattern matches that give some guarantee about the further control flow. We know that K and S are not the same. We can use them as two different constants and implement data structures using them. If we want to pattern match, we can simply put M before the expression and we can safely assume that the result is either K or S. It may happen, of course, that the expression itself doesn't reduce to K or S, in which case M doesn't reduce either, so we can't have an unexpected result.
In SKI, someone can "trick" a function by supplying a precisely crafted argument to force it spit out something bizzare. For example, in lambda calculus, we can implement ordered pair as pair = λ a b c, c a b. We can use P = pair a b to construct a pair of a and b and then use P (λ a b, a) to access the first element and P (λ a b, b) to access the second element. However, P (λ a b, x) returns x, even if x is neither a or b. Proving things about P would be very hard. We would need types and it complicates things a lot (even if we use simple types instead of dependent types).
In SKM, ordered pair can be implemented as pair = λ a b c, cases c a b (we use lambda expression for simplicity, but any lambda expression can be converted to SKM expression). Here cases is a function that takes three arguments and if the first argument reduces to K then returns the second argument, while if the first argument reduces to S then returns the third argument. Otherwise, it returns M x where x is any expression that does not reduce to K or S. We leave it as a challenge for the reader to implement cases using SKM combinators.
With this implementation of pair in SKM calculus, we can safely assume that pair a b c returns either a or b. If c is some junk value (does not reduce to K or S), then pair a b c returns M something where something is an expression that does not reduce to K or S. We treat M something like "the bottom" in Haskell. So, technically, the result is either a, or b, or bottom. This way, we can perform safe pattern matches and be able to make a theorem prover whithout having to deal with types.