# 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 `b`

in _{1}`n`

steps, and _{1}`a`

reduces to `b`

in _{2}`n`

steps, then _{2}`n`

implies _{1} = n_{2}`b`

(here _{1} = b_{2}`n`

and _{1}`n`

are natural numbers, while _{2}`b`

represents syntactical equality).
_{1} = b_{2}

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.