Try to Take

Introduction

Try to Take is a language capable of expressing different kinds of programs, including all Turing machines. It does this using a single command, a single constant (the number 1, written as I), and an arbitrarily large set of variables. Try to Take programs take no input from the user, and their output is always either 0 or 1, just enough to encode a truth value. However, unlike usual languages, Try to Take programs are impossible to reliably execute. This is because a device capable of executing all Try to Take programs could be used as an oracle, as there is a computable algorithm that can turn any Turing machine into a Try to Take program that outputs either 0 or 1 based on whether the machine halts. In fact, a certain computable algorithm can turn any PA sentence into a Try to Take program that returns 1 iff that statement about the natural numbers is actually true, and 0 otherwise.

Definitions

The central notion of Try to Take is that of "trying to take". For example, if you try to take 5 from 9, you're left with 4. In that case, trying to take is the same as substraction. However, if you try to take 9 from 5, you're left with 0; you took everything you could, but you can't go into the negatives. It's as if you tried to take 9 apples from 5 apples. This operation is also known as truncated subtraction, doz (difference or zero), and monus, according to Wikipedia. Trying to take can be defined as max(a-b,0) and is often notated as ∸ (minus with a dot on top of it).

However, trying to take is not the actual, sole command of Try to Take; instead, "monuseries", symbolized by a capital M, is. Monuseries work a bit like infinite series do in math; however, instead of being repeated addition, it's repeated monus, a.k.a. "try to take". For example: $1\ {\underset {x}{M}}\ x$ would be interpreted as "...(((1 monus 0) monus 1) monus 2)...", with the part following ${\underset {x}{M}}$ repeatedly evaluated with x as the next natural number. If at some point, the result of trying to take is zero, the computation can be stopped, as it will stay as 0 forevermore (monus can never increase the value). Alternatively, if at some point, the remaining terms we're trying to take are all 0, the computation stops too, as the the result will never decrease below the current value. One of these cases must always happen, though it is in general undecidable which. For specific expressions, this can often be figured out, however.

Examples of monuseries

$1\ {\underset {x}{M}}\ x$ = 1∸0∸1∸2∸... = 0

$16\ {\underset {x}{M}}\$(3∸x) = 16∸(3∸0)∸(3∸1)∸(3∸2)∸(3∸3)∸(3∸4)∸... = 16∸3∸2∸1∸0∸0∸... = 10

Note that the second monuseries is not by itself valid in Try to Take, and the first monuseries should be written with an I in the place of the first 1.

Language specification

A single Try to Take term is one of the following:

• $I$ (taken to have the value 1)
• a variable $(x,y,z,...)$
• $(\mathrm {term1} \ {\underset {variable}{M}}\ \mathrm {term2} )$

With $\mathrm {term1}$ and $\mathrm {term2}$ denoting other Try to Take terms and $variable$ denoting a variable name.

A Try to Take program is a term that fulfills the following condititions:

• All variables are bound to some monuseries.
• No $\mathrm {term2}$ of a monuseries contains anywhere in it a second monuseries using the same variable name as the first one.

The output of a Try to Take program is taken to be its value when evaluated. It is trivial to show that this means the output is always 0 or 1.

Notations

When casually writing down terms and programs, extra brackets may be removed, such as the outermost ones. In the case of $I\ {\underset {x}{M}}\ x\ {\underset {y}{M}}\ y$, this is to be understood as $(I\ {\underset {x}{M}}\ x)\ {\underset {y}{M}}\ y$.

Instead of using variable names, the variables may be numbered. Using this method, $I\ {\underset {x}{M}}\ x\ {\underset {y}{M}}\ y$ can be written as $I\ {\underset {1}{M}}\ 1\ {\underset {2}{M}}\ 2$.

All variables can be denoted with the letter x by using tabulation and marking which monuseries different variables are bound to using |. The previous example can thus be written as:

I
M
|  x
M
|  x

Had the example been $I\ {\underset {x}{M}}\ (x\ {\underset {y}{M}}\ y)$, it would've been written as:

I
M
|  x
   M
   |  x

Abbreviations

Once some kind of a function or operation has been defined with a T2T term, more terms may be written using this function in the context of analyzing T2T, with the intention that uses of the function would be replaced by its definition when actually creating a T2T program.

Translation of PA sentences

Note that monus can itself be defined using just monuseries. Note how y does not appear in the monuseries; this trick was first pointed out by User:Patcail.

a∸b can be defined as $a\ {\underset {x}{M}}\ (b\ {\underset {y}{M}}\ x)$

Truth functions are straightforward, with 0 used to encode falsehood and 1 used to encode truth.

$0$ can be defined as $I\ {\underset {x}{M}}\ I$

$1$ can be defined as $I$

$\neg a$ can be defined as $I\ {\underset {x}{M}}\ a$

$a\wedge b$ can be defined as $a\ {\underset {x}{M}}(I\ {\underset {y}{M}}\ b)$

$a\vee b$ can be defined as $I\ {\underset {x}{M}}(I\ {\underset {y}{M}}\ a\ {\underset {z}{M}}\ b)$ or just $\neg (\neg a\wedge \neg b)$

$a\implies b$ can be defined as $I\ {\underset {x}{M}}(a\ {\underset {z}{M}}\ b)$ or just $\neg a\vee b$

Abbreviation will be used here for writing out the definitions for equality and inequalities.

$a=0$ can be defined as $I$∸$a$

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a=b} can be defined as Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle (a} ∸Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle b=0)\wedge(b} ∸Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a=0)}

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a > 0} can be defined as Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \neg(a=0)}

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a < b} can be defined as Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle b} ∸Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a>0}

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a\le b} is defined as: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a=b\lor a<b}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle a\ne b} is defined as: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \lnot(a=b)}

Quantification is necessary for expressing many concepts. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \text{gate}} is of interest for Method 2, as described below.

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall x, \varphi(x)} is defined as: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle I\ \underset x M\ \lnot\varphi(x)}
$\exists x,\varphi (x)$ is defined as: $\lnot \forall x,\lnot \varphi (x)$
${\text{gate}}(p,a)$ is defined as: $a\ {\underset {x}{M}}\ \lnot p$

Arithmetical operations - Method 1

With Method 1, results of operations like a+b cannot be defined directly, which follows from the inability of monuseries to provide a result higher than the left term. Instead, propositions like a+b=c are defined, and sentences of PA are turned into equivalent ones that do not directly use the results of expressions. Quantification is the primary tool used to accomplish this, as demonstrated with +.

$a+b=c$ can be defined as $c$∸$a=b\wedge c$∸$b=a$

Then, with P symbolizing an arbitrary proposition and x an unused variable name,

$P(a+b)$ can be rewritten as $\forall x(a+b=x\implies P(x))$

The same strategy works for multiplication and can be repeated until the expression has been rewritten into a desirable form. As such, with the following definition, it is established that all of PA can be expressed using T2T terms:

$a\cdot b=c$ can be defined as $\forall d(c+1=d\implies (d\ {\underset {e}{M}}\ (a\ {\underset {f}{M}}\ \neg (b>e)))=1)$ with $d,e,f$ symbolizing unused variables.

Arithmetical operations - Method 2

With Method 2, results of operations can be defined as unary predicates over expressions. For example, $a+b$ is defined as a unary predicate that holds only for those expressions $c$ for which $c=a+b$. Since the set of all expressions is countably infinite, the unary predicates over expressions form a set. In order to compose the operations, we can use the do notation inside the Set monad, with Haskell-like notation.

Addition is defined as:

${\begin{aligned}&a+b={\text{do}}\\&\quad r\leftarrow U\\&\quad {\text{guard }}{a=r\mathop {\dot {-}} b}\\&\quad {\text{guard }}{b=r\mathop {\dot {-}} a}\\&\quad {\text{return }}r\end{aligned}}$

The $U$ is the set of all expressions. The guard is a part of the Alternative monad, returning the empty set if the condition fails. The return is the standard $\eta$ natural transformation of the Set monad. We can express natural transformation in terms of expressions:

${\begin{aligned}&\eta =\lambda xr,r=x\\&\mu =\lambda fgr,\exists z,f(z)\land g(z,r)\end{aligned}}$

The mapping of morphisms for the Set endofunctor is defined as ${\text{fmap}}=\lambda fgr,\exists z,g(z)\land r=f(z)$.

The inverse of a monomorphic function is defined as:

${\begin{aligned}&f^{-1}(b)={\text{do}}\\&\quad a\leftarrow U\\&\quad {\text{guard }}b=(\leftarrow f(a))\\&\quad {\text{return }}a\end{aligned}}$

Subtraction: $a-b=(\lambda x,b+x)^{-1}(a)$
Multiplication by two: $2\cdot a=a+a$
Division by two: ${\frac {a}{2}}=(\lambda x,2\cdot x)^{-1}(a)$

Square of a number:

${\begin{aligned}&a^{2}={\text{do}}\\&\quad r\leftarrow U\\&\quad {\text{guard }}1=r\ {\underset {x}{M}}\ {\text{gate}}(x\leq a,x)\\&\quad (\leftarrow 2\cdot (\leftarrow r-1))-a\end{aligned}}$

Multiplication:

${\begin{aligned}&a\cdot b={\text{do}}\\&\quad x\leftarrow a^{2}\\&\quad y\leftarrow b^{2}\\&\quad z\leftarrow (\leftarrow a+b)^{2}\\&\quad \left({\frac {\leftarrow z-(\leftarrow x+y)}{2}}\right)\end{aligned}}$

Constant $2$ is defined as $(\leftarrow 1+1)$
Division: ${\frac {a}{b}}=(\lambda x,b\cdot x)^{-1}(a)$
Divisibility $a|b$ is defined as $\exists k,b=(\leftarrow a\cdot k)$
Parity check ${\text{Even}}(a)$ is defined as $(\leftarrow 2)|a$
Primality check ${\text{Prime(a)}}$ is defined as $\forall k,k|a\to (k=1)\neq (k=a)$

Explanation

A unary predicate is a Try to Take expression that contains at most one free variable. For example 0 < x, where x is a free variable. Even though a final Try to Take program cannot contain free variables, unary predicates can be used to construct inner expressions. Each unary predicate can be understood as the set of all expressions for which the predicate, when parametrized with that expression, evaluates to a truthy value (constant 1). To facilitate constructing expressions using unary predicates, we introduce the do-notation syntax, used in functional languages when working with monads. In fact, the class of countable sets, when regarded as containers, form a covariant endofunctor with monadic natural transformations. Therefore, we can use the Set monad to compose unary predicates just like ordinary functions.

We already defined the universal and the existential quantifier. Let U = I. Here, U (standing for the universal set) is also a unary predicate (it contains no free variables, which fits the definition of "at most one free variable"). Therefore, U can be regarded as the set of all expressions, since for all expressions it evaluates to 1.

The return e, where e is a Try to Take expression, translates to x = e, where x is a fresh variable that does not appear in e. It represents the singleton set that contains exactly expression e.

The guard e, where e is an expression, translates to $e\land x=I$. If e is a truthy value (positive), then guard e is the singleton set containing only 1. Otherwise, it is the empty set.

Now we introduce two additional operators. First, the functorial mapping, usually called fmap. Given a unary predicate S (a set of expressions) and a function f over expressions, the fmap f S is defined as $\exists z,S(z)\land r=f(z)$. Here r is the free variable of the newly constructed unary predicate (the result of fmap) and S(z) represents the expression S whose free variable is replaced with variable z (assuming z does not occur in S or f). Similarly, f(z) represents the expression f whose free variable is replaced with variable z. This represents the image of set S under function f.

The second operator that we define is the monadic binding operator S >>= f, where S is a unary predicate (a set) and f is a binary predicate (predicate over sets of expressions). It translates to $\exists z,S(z)\land f(z,r)$, where r is the new free variable of the resulting unary predicate.

Finally, we define the do-notation as a series of monadic binding operators. The syntax

${\begin{aligned}&{\text{do}}\\&\quad x\leftarrow e\\&\quad f(x)\end{aligned}}$

translates to e >>= f. The binding operator is left-associative.

Besides the fancy syntax, this approach is equivalent to Method 1. The only exception is that when translating unary predicates to expressions, in Method 1 we use the universal quantifier, while in Method 2 we use the existential quantifier. For example, the addition $P(a+b)$ in Method 1 translates to $\forall x,x=a+b\to P(x)$, while in Method 2 it translates to $\exists x,x=a+b\land P(x)$. These two translations are equivalent as long as the unary predicate holds for exactly one value (e.g. there exists exactly one c such that c = a + b).

As an example, let's analyze the definition of addition in Method 2 and compare it to the one from Method 1. Recall that we defined addition as

a + b = do
  r ← U
  guard a = r ∸ b
  guard b = r ∸ a
  return r

We start from the return. Since return e is defined as x = e, where x is a fresh variable not appearing in e, we can choose a new variable x and replace return r with x = r. Then, replace guard a = r ∸ b with a = r ∸ b ∧ y = I and replace guard b = r ∸ a with b = r ∸ a ∧ z = I (here y and z are fresh variables). Replace U with I. Now we have

a + b = do
  r ← I
  a = r ∸ b ∧ y = I
  b = r ∸ a ∧ z = I
  x = r

For the two expressions obtained by guards we do not have bound variables, so we can introduce any fresh variables we want:

a + b = do
  r ← I
  q ← a = r ∸ b ∧ y = I
  w ← b = r ∸ a ∧ z = I
  x = r

Now we recursively expand the definition of the binding operator. The first step:

a + b = do
  r ← I
  q ← a = r ∸ b ∧ y = I
  ∃ w, b = r ∸ a ∧ w = I ∧ x = r

The second step:

a + b = do
  r ← I
  ∃ q, a = r ∸ b ∧ q = I ∧ ∃ w, b = r ∸ a ∧ w = I ∧ x = r

The final step:

a + b = ∃ r, I ∧ ∃ q, a = r ∸ b ∧ q = I ∧ ∃ w, b = r ∸ a ∧ w = I ∧ x = r

Simplifying the expression we obtain:

a + b = ∃ r, a = r ∸ b ∧ b = r ∸ a ∧ x = r

which is equivalent to the definition from Method 1. It is a predicate whose free variable is x.

Multiplication is different though. In Method 2 we defined multiplication as

$a\cdot b={\frac {(a+b)^{2}-(a^{2}+b^{2})}{2}}$

and the square is defined as

$a^{2}=2\sum _{i=0}^{a}i-a$

The sum is defined using gate.

Goldbach's conjecture

${\begin{aligned}&{\text{Goldbach}}=\forall n,\\&\quad ({\text{do}}\\&\quad \quad {\text{guard }}{\text{Even}}(n)\\&\quad \quad (\leftarrow 2)<n\\&\quad )\to \exists ab,{\text{do}}\\&\quad \quad {\text{guard }}{\text{Prime}}(a)\land {\text{Prime}}(b)\\&\quad \quad n=(\leftarrow a+b)\end{aligned}}$

The correctness of this implementation is verified using the Lean theorem prover.

External resources

• Implementation written by User:Hakerh400