Entrance

**Entrance**
Paradigm(s)	Declarative
Designed by	User:Hakerh400
Appeared in	2020
Computational class	Turing complete
Major implementations	Interpreter
File extension(s)	`.txt`

Entrance is an advanced fully automatic theorem prover.

Overview

Source code contains one or more function definitions.

Expression

Expression can be one of:

Constant
Pair
Variable
Function call

Constant is represented as a non-negative integer. Constants are not related to each other and they cannot be compared or sorted. We cannot implicitly find the successor of 0 for example. Constants are used as unique identifiers. Two constants are equal iff they have the same representation in the source code (represent the same integer). Example of a constant: 123

Pair contains two expressions. Two pairs are equal iff their first elements are equal and their second elements are equal. Example of a pair: (5, 7)

Variable is a placeholder that can contain any expression. A variable can be substituted by any other expression as long as it is done consistently in that function definition. Example of a variable: x

Function call is a transformation of an expression. Example of a function call: f 5 (it means that function f is applied to expression 5)

Statement

Statement is a top-level expression (not nested in a pair or a function call).

Function definition

Source code contains function definitions. Each function definition consists of left-hand-side, then an equal sign, then right-hand-side and ends with a semicolon. Left-hand-side is a function call and right-hand-side is any expression. For example:

f x = (x, x);

This is a function that takes any variable x and produces a pair containing x as both elements. Multiple definitions of the same function are allowed.

Computation

Input is a single statement that is to be proved. Output is the input statement with all function calls eliminated by applying function definitions.

If the statement is provable, the interpreter will find and output a proof (does not need to be the shortest proof). If the statement is unprovable within the system, the interpreter may or may not be able to detect that, so it may never halt.

Syntactic sugar

Strings can be used to denote unique symbols. For example, "abc" is a unique symbol, like a constant integer.

Basic examples

The definitions above may not be clear, but it should be more obvious how the prover works once we see the examples.

Function application

Given the following source code that we posted before:

f x = (x, x);

and the following input statement:

f 0

The output will be:

(0, 0)

Explanation: expression f 0 is transformed into (0, 0) by applying the first function definition for x: 0. So far, one may think that Entrance is a simple functional language. However, in the next examples we will show how to actually implement a formal mathematical system.

Reversed function application

Source code:

f x = (x, x);
g f x = x;

Input statement:

g (0, 0)

Output:

Explanation: now we see a reversed function application. Function g takes the output of f applied to some variable x and then returns that x. In our example, (0, 0) must be the output of f called with something. Function g finds that something and returns it.

If we tried to prove g 0 or g (0, 1), we would get the "No solution exists" message, because neither 0, nor (0, 1) can be an output of f. If we tried to prove g ((3, 3), (3, 3)), we would get (3, 3) as the output.

Indeterminate definition

Source code:

f x = y;

Input:

f 0

In this example, output can be any expression, because y is not related to x in any way.

Recursive expression construction

Code:

f 0 = (0, 0);
f g x = (x, x);
g f x = x;

Here we have three function definitions.

Function f when called with 0 returns (0, 0). When called with something that is the return value of g called with some x, then returns (x, x). In other words, function f asserts that the argument that is passed to it is either 0, or is obtained by applying f to something (because g is an inverse of f).

In this system, statements g (0, 0), g ((0, 0), (0, 0)), and similar are provable, while, for example, g 0 is not provable (because 0 cannot be an output of f).

Assertions

Code:

f (x, x) = x;

Function f takes a pair of two identical elements. Therefore, we assert that both elements must be the same. Statements like f (0, 0), f (1, 1), f ((5, 5), (5, 5)) are provable, while f 0, f (1, 2), f ((1, 1), (2, 2)) are not provable.

Advanced examples

Now it is time to show how to implement some real mathematical systems. We first define inference rules that exist in the system. Each inference rule has zero or more premises and a conclusion. Axioms (or axiom schemas) are inference rules that have no premises.

Łukasiewicz system

In this example we will use a simplified version of Łukasiewicz system. We define the following inference rules (the first two are axioms because they have no premises and the third one is Modus ponens):

${\begin{aligned}&\vdash x\to (y\to x)\\&\vdash (x\to (y\to z))\to ((x\to y)\to (x\to z))\\x,x\to y&\vdash y\end{aligned}}$

Our goal is to prove that $x\to x$ . However, because there are no quantifiers (we did not define them in this system), instead of proving that $x\to x$ for any $x$ , it is enough to prove that it is true for a single unique constant, for example $5\to 5$ .

Now, the question is how to represent implication in our program. Given that the implication is the only operator in this system and given that it has exactly two operands, we can use a pair to denote implication. For example, $A\to B$ can be represented in our program as (A, B).

When we talk about proving a statement in this system, we need to define what we expect as the output. Not only that we want to know whether the statement is provable, but we also want to know which inference rules are applied and in which order. Keeping in mind that the output will contain only pairs and constants, we need to encode inference rules as unique constants, so that we can recognize them in the output. For example, we can say that the first inference rule has identifier 10, the second one has identifier 20 and the third one (Modus ponens) has identifier 30.

In the output, we want (10, (x, y)) (where x and y have concrete values) to represent an application of the first inference rule (the first axiom) to expressions x and y. Similarly, we want (20, (x, (y, z))) to represent an application of the second inference rule to expressions x, y and z. Finally, we want (30, (A, B)) to represent an application of Modus ponens to A and B, where A is the proof of some x and B is the proof of the implication (x, y) for some y.

This is our program:

f (10, (x, y)) = (x, (y, x));
f (20, (x, (y, z))) = ((x, (y, z)), ((x, y), (x, z)));
f (30, (g x, g (x, y))) = y;
g f x = x;

Explanation: function f represents inference rule application, while g is an inverse of f. Function g returns a proof of its argument. Now, if we look closer at function f, we can see that it strictly follows our definition from the previous paragraph. Rule 10 (the first axiom) can be applied to any expressions x and y. Rule 20 (the second axiom) can be applied to any expressions x, y and z. Rule 30 (Modus ponens) can be applied to proofs of x and (x, y), yielding y.

Input statement:

g (5, 5)

Here 5 is just a random identifier, because we have not defined any quantifiers (for simplicity), so it is enough to prove the statement for some unique identifier. If we run the program, we would get the following output:

(30, ((10, (5, 0)), (30, ((10, (5, (0, 5))), (20, (5, ((0, 5), 5)))))))

It may seem a bit complicated, but let's analyze it and rewrite the obtained proof in a mathematical syntax. First, we can add spacing and format it better for readability:

(30, (                      // Modus ponens
  (10, (5, 0)),             // Axiom 1
  (30, (                    // Modus ponens
    (10, (5, (0, 5))),      // Axiom 1
    (20, (5, ((0, 5), 5)))  // Axiom 2
  ))
))

The first thing we may notice is the identifier 0 appearing out of nowhere. That is because there are more than one possible proof and the prover decided to use 0 for expressions that can be anything. It could decide to use any other expression, as long as it does not violate inference rules.

What we can see from the above proof is that we apply five inference rules. It is easier to read from the end, because that is how you would prove it manually. We first apply the first axiom to x: 5 and y: (5, 0). Then we apply the second axiom to x: 5, y: (0, 5) and z: 5. Then we apply Modus ponens to the two obtained expressions. Then we again apply the first axiom, but this time to x: 5 and y: 0. Finally, we apply the Modus ponens again, obtaining the expression that we wanted to prove. This proof can be written using mathematical syntax:

${\begin{aligned}&1.{\text{A1}}:5\to (0\to 5)\\&2.{\text{A1}}:5\to ((0\to 5)\to 5)\\&3.{\text{A2}}:(5\to ((0\to 5)\to 5))\to ((5\to (0\to 5))\to (5\to 5))\\&4.{\text{MP}}[2,3]:(5\to (0\to 5))\to (5\to 5)\\&5.{\text{MP}}[1,4]:5\to 5\end{aligned}}$

The next step would to be introduce negation and prove some statements involving negation. However, since we would have two different operators (implication and negation), we could no longer use a simple pair to represent implication. We would need to introduce some unique identifiers for implication and negation (for example 0 for implication and 1 for negation). Then, we would represent $A\to B$ as (0, (A, B)) and $\lnot A$ as (1, A). Operators cannot be confused with other identifiers, because operators require a pair, while identifiers are just literal constants.

Proving commutativity of equality

In this example we show how to define equality as an operator and how to prove the commutative property of equality. Since equality is an operator and since it is the only operator in this example, we can use a simple pair to denote it, meaning that $A=B$ can be represented as (A, B).

First, we need to define what equality actually means. We can say that two expressions are equal iff all statements that are true for the first expression are also true for the second expression. However, that would require us to define quantifiers, which are out of scope for this example. So, we only define the equality in one direction, meaning that if two expressions x and y are equal and some statement P parametrized with x and y is provable, then we can conclude that P parametrized with y and x is also provable (we basically swap the parameters).

The question now is how to define a parametrized statement. What we actually want is a statement containing some expressions, but which also can contain two placeholders that can be substituted with concrete values. Therefore, we can define parametrized statement in the following way:

0 - Represents the first parameter
1 - Represents the second parameter
(0, m) - means that m is an expression that is not parametrized
(1, (m, n)) - means that (m, n) is a pair of two parametrized statements

Then, we need a function that will take a parametrized statements and two expressions and return the statement with the expressions substituted into it. We call that function subst.

Finally, we need to define inference rules. We want to prove that from $A=B$ we can conclude $B=A$ . However, since we do not have implication now, we can define $A=B$ as an axiom. So, we have two inference rules:

${\begin{aligned}&\vdash A=B\\x=y,P_{x,y}&\vdash P_{y,x}\end{aligned}}$

and we want to prove that $B=A$ . Of course, it is trivial, but we show this example to demosntrate substitution. We use identifier 5 to denote A and 7 to denote B. This is our program:

f 10 = (5, 7);
f (20, ((P, (x, y)), (g (x, y), g subst (P, (x, y))))) = subst (P, (y, x));
g f x = x;

subst (0, (x, y)) = x;
subst (1, (x, y)) = y;
subst ((0, m), xy) = m;
subst ((1, (m, n)), xy) = (subst (m, xy), subst (n, xy));

Explanation: the first inference rule is denoted by identifier 10, while the second inference rule is denoted by a pair containing identifier 20 and a proof of the premises. Function subst follows the algorithm explained above for substituting expressions into a parametrized statement. The xy represents (x, y), but since we do not need to extract any of them, we can use a single variable xy.

When we run this program with input statement g (7, 5), we will get the following proof:

(20, (((1, (0, 1)), (5, 7)), (10, 10)))

Let's analyze it in details. We have three inference rule applications:

(20, (                    // Second rule
  ((1, (0, 1)), (5, 7)),  // P, x and y
  (10, 10)                // Proofs for x = y and P_x,y
))

First, the prover has proved that $A=B$ (remember that 5 denotes $A$ and 7 denotes $B$ ) by applying the first axiom (which literally says exactly that). Then the prover constructed a parametrized statement $P$ defined as $P_{x,y}:(x=y)$ . Therefore, $P_{A,B}:(A=B)$ is true. Then the prover used the second inference rule to conclude that $P_{B,A}:(B=A)$ is also true. That is the end of the proof.

Zermelo–Fraenkel set theory

It is certainly possible to model the ZFC system. We showed how to implement implication, equality, parametrized statements and substitutions. We also showed assertions and expression transformation via inference rules.

However, it is not so easy to implement ZFC, because the nine axioms of the ZFC are not enough. Entrance does not know anything about quantifiers, equivalence operator and logical operators. For each logical operator we need to define inference rules. For universal and existential quantifiers we need to also define at least two inference rules to specify how they behave and we would need to use parametrized statements to model bound variables. For each operator, we would need to introduce a new unique identifier and we would probably need another program which would transform the Entrance proof to something humans can easily read and understand.

Also, the axiom of choice would be problematic, because it does not state anything about how the choice function is to be constructed. It simply states that such a function exists. The axiom of choice can be formally represented in many different ways, but if the ZFC is inconsistent, the way we formally represent the axiom of choice may influence the consistency of ZFC.

Other examples

Find a path in a 2D grid

Source code:

f "start" = (0, 0);
f (g (x, S y), "up") = (x, y);
f (g (x, y), "right") = (S x, y);
f (g (x, y), "down") = (x, S y);
f (g (S x, y), "left") = (x, y);

g f x = x;

S x = ("S", x);

Input: g (S 0, S 0);

Possible output: (((("start", "right"), "right"), "down"), "left")

Explanation: We defined an infinite 2D grid. A virtual agent is positioned in the top left square (grid extends infinitely to the right and the bottom). Basically, 0 represents the top (or leftmost) coordinate, S 0 represents the next coordinate, S S 0 the next coordinate, and so on. In this example, we want to find a path to the point $\left(1,1\right)$ , which is represented as (S 0, S 0), so the agent outputs a sequence of moves that leads to that point. Note that the path may not be the shortest possible (as we can see, the output path has 4 moves, but it can obviously be solved in 2 moves - it depends on the heuristic and/or random number generator used by the interpreter).

Generate a palindrome

Source code:

length 0 = (0, (0, (0, (0, (0, (0, (0, 0)))))));

f x = and ( and ( and (
  isPalindrome x,
  hasTwoDifferentChars x),
  hasOnlyAB x),
  eq (len x, length 0)
);

g f x = x;

and (0, x) = 0;
and (1, x) = x;

or (0, x) = x;
or (1, x) = 1;

isPalindrome 0 = 1;
isPalindrome (x, 0) = 1;
isPalindrome (x, append (y, x)) = isPalindrome y;

append (0, c) = (c, 0);
append ((a, b), c) = (a, append (b, c));

eq ((a, b), (c, d)) = eq (b, d);
eq ((a, b), 0) = 0;
eq (0, (a, b)) = 0;
eq (0, 0) = 1;

len 0 = 0;
len (x, y) = (0, len y);

hasTwoDifferentChars x = and (
  has (x, "A"),
  has (x, "B")
);

hasOnlyAB 0 = 1;
hasOnlyAB ("A", x) = hasOnlyAB x;
hasOnlyAB ("B", x) = hasOnlyAB x;

has (0, c) = 0;
has (("A", b), "A") = 1;
has (("A", b), "B") = has (b, "B");
has (("B", b), "A") = has (b, "A");
has (("B", b), "B") = 1;

Input: g 1;

Output: A palindrome (possibly randomly generated) of length 7 that contains only letters A and B. For example, the output may look like this: ("A", ("B", ("B", ("A", ("B", ("B", ("A", 0)))))))

Generate a permutation of decimal digits

Source code:

digit 0 = 0;
digit (0, a) = 0;
digit (0, a) = digit a;

and (a, 0) = 0;
and (a, 1) = a;

or (a, 0) = a;
or (a, 1) = 1;

eq ((a, b), (c, d)) = eq (b, d);
eq ((a, b), 0) = 0;
eq (0, (a, b)) = 0;
eq (0, 0) = 1;

len 0 = 0;
len (x, y) = (0, len y);

isArr (arr, length) = and (
  eq (len arr, length),
  hasDigits (arr, length)
);

generateArr if (
  isArr (arr, length),
  (length, "null")
) = arr2str arr;

if (0, (a, b)) = b;
if (1, (a, b)) = a;

hasDigits (arr, 0) = 1;
hasDigits (0, (a, b)) = 0;
hasDigits (arr, (0, a)) = and (
  hasDigit (arr, (0, a)),
  hasDigits (arr, a)
);

hasDigit (0, c) = 0;
hasDigit ((a, b), c) = or (
  eq (a, c),
  hasDigit (b, c)
);

arr2str 0 = 0;
arr2str (a, b) = (digit2str a, arr2str b);

digit2str 0 = 0;
digit2str (a, b) = strNext digit2str b;

strNext 0 = 1;
strNext 1 = 2;
strNext 2 = 3;
strNext 3 = 4;
strNext 4 = 5;
strNext 5 = 6;
strNext 6 = 7;
strNext 7 = 8;
strNext 8 = 9;

Input: generateArr (0, (0, (0, (0, (0, 0)))));

Output: (1, (2, (5, (4, (3, 0)))))

Generate a random bit

Source code:

f 0 = 0;
f 0 = 1;

Input: f 0;

Output: Either 0 or 1.

Increment/decrement binary number

Source code:

inc a = trim inc1 a;
dec inc1 a = trim a;

inc1 a = if (snd add1 a, (
  (1, fst add1 a),
  fst add1 a
));

trim 0 = 0;
trim (0, a) = trim a;
trim (1, a) = (1, a);

fst (a, b) = a;
snd (a, b) = b;

if (0, (a, b)) = b;
if (1, (a, b)) = a;

add (a, 0) = (a, 0);
add (0, 1) = (1, 0);
add (1, 1) = (0, 1);
add ((a, b), 1) = ((fst add2 (a, b), fst add1 b), snd add2 (a, b));

add1 a = add (a, 1);
add2 (a, b) = add (a, snd add1 b);

Input: inc (1, (0, (1, (0, (0, (1, 1))))))
Output: (1, (0, (1, (0, (1, (0, 0))))))

Input: dec (1, (0, (0, (0, (1, (0, 0))))))
Output: (1, (0, (0, (0, (0, (1, 1))))))

Applications

Entrance can be used for a lot of different tasks. For example, it can be used to make an interpreter for Halt halt halt. It can be used to make a program that searches (not guaranteed to halt) for a solution to any NP-hard problem, such as

Determine whether a given Turing-machine halts
Determine whether two lambda expressions are equivalent
Determine whether a given Post correspondence problem has a solution
Determine whether two given programs give identical outputs for all inputs
Determine whether two given function in ƎↃИAЯT are equivalent

Interpreters

Interpreter

Entrance

Contents

Overview

Expression

Statement

Function definition

Computation

Syntactic sugar

Basic examples

Function application

Reversed function application

Indeterminate definition

Recursive expression construction

Assertions

Advanced examples

Łukasiewicz system

Proving commutativity of equality

Zermelo–Fraenkel set theory

Other examples

Find a path in a 2D grid

Generate a palindrome

Generate a permutation of decimal digits

Generate a random bit

Increment/decrement binary number

Applications

Interpreters

Navigation menu

Entrance

Overview

Expression

Statement

Function definition

Computation

Syntactic sugar

Basic examples

Function application

Reversed function application

Indeterminate definition

Recursive expression construction

Assertions

Advanced examples

Łukasiewicz system

Proving commutativity of equality

Zermelo–Fraenkel set theory

Other examples

Find a path in a 2D grid

Generate a palindrome

Generate a permutation of decimal digits

Generate a random bit

Increment/decrement binary number

Applications

Interpreters

Navigation menu

Search