SKM Calculus

Paradigm(s) Functional User:Hakerh400 2022 Turing complete Implemented `.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.