Π₁

Π₁

Paradigm(s)	Declarative
Designed by	User:Hakerh400
Appeared in	2022
Computational class	Category:Turing complete
Major implementations	Implementation in Haskell
File extension(s)	.txt

Π₁ is a dependently typed set-theoretic declarative programming language with inductive constructions.

Overview

In this language, everything is a class. A class is either a proper class, or a set.

A set is a collection of (countably or uncountably many) other sets. A set can be empty. Every set has an ordinal rank. Two sets are equal iff they contain the same elements.

Constructing sets

There are several ways to make a set.

Literal

The simplest way is to explicitly provide its elements. For example, $\left\{A,B,C\right\}$ is the set that contains exactly $A$, $B$ and $C$ (assuming they are sets that we have already defined). The empty set is represented as $\left\{\right\}$.

Union

If $A$ is a set, then $\bigcup A$ is the union of all elements of $A$.

Powerset

If $A$ is a set, then ${\mathcal {P}}(A)$ is the set of all subsets of $A$.

Choice function

To pick an element from a nonempty set, we prepend question mark before it.

If $A$ is a nonempty set, then ?A is an element of $A$. If $A$ is the empty set, the result is implementation-dependent. The choice function always returns the same result for the same set.

λ-functions

An ordered pair of two sets $A$ and $B$ is defined as $\left\{A,\left\{A,B\right\}\right\}$. Set $A$ is called the first element, and $B$ is called the second element.

Let $A$ be a set and ${\mathcal {F}}$ be a function (in an informal sense) that maps each element of $A$ to some set. In other words, $\forall (x\in A),({\mathcal {F}}(x){\text{ is a set}})$.

A function $f$ that maps each $x\in A$ to an element of set ${\mathcal {F}}(x)$ is a set of ordered pairs such that for each pair $(x,y)$:

• $x\in A$
• $y\in {\mathcal {F}}(x)$

Additionally, each $x\in A$ appears in exactly one pair as the first element.

Example of a function:

λ (x ∈ A), $\varphi$

Expression $\varphi$ constructs a set and may contain $x$ as a free variable.

Each λ-function is a set.

Π-functions

Example:

Π (x ∈ A), $\varphi$

Expressions $\varphi$ constructs a set and may contain $x$ as a free variable. A Π-function is the minimal set satisfying

(λ (x ∈ A), $\psi$) ∈ (Π (x ∈ A), $\varphi$)

Basically, Π-function is the ${\mathcal {F}}$ of a lambda function.

Each Π-function is a set.

Non-dependent function type

If $A$ and $B$ are sets, then A → B is a syntactic sugar for $(\Pi (x\in A),B)$. In general, if $x$ does not appear free in $\varphi$, then

$(\Pi (x\in A),\varphi )\equiv (A\to \varphi )$

Application

Let $A$ be a set and $f\in \Pi (x\in A),{\mathcal {F}}(x)$ for some ${\mathcal {F}}$.

Expression $f(x)$ represents function application (parentheses around $x$ are optional). It satisfies the following condition: $f(x)=y\Longleftrightarrow (x,y)\in f$.

Comprehension

Let $A$ be a set and $f\in \Pi (x\in A),{\mathcal {F}}(x)$ for some ${\mathcal {F}}$.

$\left\{x\in A\mid f(x)\right\}$ is the set of exactly the elements $x\in A$ for which $f(x)$ is nonempty.

Map

Let $A$ be a set and $f\in \Pi (x\in A),{\mathcal {F}}(x)$ for some ${\mathcal {F}}$.

$\left\{x\in A;f(x)\right\}$ is the set that contains $y$ if and only if $\exists (x\in A),f(x)=y$.

Inductive constructions

We introduce yet another syntax for making sets:

$\left\{x_{1},x_{2},x_{3},\dots \,\lambda x,\varphi \right\}$

Note that every lambda expression must have the membership ($\in$) defined for each parameter. Here, we don't have the membership for $x$, so $x$ actually represents any element of the set being defined. Expression $\varphi$ constructs a set and $x$ may appear free in $\varphi$. The result is the smallest set (with the smallest number of elements) that contains all the constant terms $x_{1},x_{2},x_{3},\dots$, plus all elements that can be inductively constructed using the lambda expression provided.

Definitions

To define a set, write an identifier followed by := and then the definition. For example:

A := {}
B := {A}
C := {A, B}

We defined three sets. Set $A$ is empty. Set $B$ is a singleton set that contains $A$. Set $C$ is equal to $\left\{\left\{\right\},\left\{\left\{\right\}\right\}\right\}$.

To define a proper class, we add set parameters to the left. For example:

my_class S := {S}

This can be understood as a meta function that takes a set $S$ and makes a singleton set that contains $S$. Note that my_class is not a set, so in a set expression it must always be supplied with enough arguments.

Basic examples

First, we can make the empty set:

emp := {}

Then we can make propositions false and true

false := emp
true := {false}

Proposition false is the empty set. Proposition true is the singleton set that contains the empty set. We can make the set of all propositions:

prop := {false, true}

It has exactly two elements. Now we want to define a function that can tell us whether the given set is empty. If the set is empty, it should return true, and otherwise it should return false. But, if we want it to work for any set, then that function itself cannot be a set. It must be a proper class:

is_empty S := λ (a ∈ S), a → false

So, what did we do here? We defined a proper class is_empty, which is a meta function parametrized with some set $S$. Let $S$ be some set. Then is_empty S is a function that takes an element $a\in S$ and returns (a → false) (if the supplied argument is not a member of $S$, the result if implementation-dependent). Now, what does (a → false) mean? It is a syntactic sugar for (Π (x ∈ a), false), which represents the set of all functions from elements of a to elements of false. Since false is the empty set, if a is nonempty, then there is no such function, so (a → false) is the empty set. However, if a is empty, then there exists a single function (function from the elements of the empty set to the elements of the empty set), which is represented as the empty set itself, so the result of (a → false) is the set that contains the empty set (which is true by definition).

Note that, despite the fact that is_empty is a proper class, is_empty S is a set, so is_empty X (is_empty S) is a valid expression. But in order to guarantee a valid result, we must provide as X a set that contains is_empty S, which can be {is_empty S}. So, is_empty {is_empty S} (is_empty S) is a valid set and it is equal to false.

Another way to write is_empty

is_empty S (a ∈ S) := a → false

It is equivalent to the previous definition. Whenever the right-hand-side starts with a lambda expression, we can move the argument to the left-hand-side and remove lambda. Note that the definition does not change. is_empty S is still a set (function) for any set $S$. However, if we removed ∈ S, then it would become a two-parameter proper class is_empty S a := a → false (in that case, is_empty S would still be a proper class).

Next, we can define logical negation:

not := is_empty prop

It is basically is_empty specialized to work on propositions. Now, we define nonempty, which returns true iff the given set is nonempty:

nonempty S (a ∈ S) := not (is_empty S a)

Note that nonempty can be used to convert any set to a proposition. The next thing we want to define are logical operators. Let's start with implication. For any two propositions a and b, implication imp a b is true iff a is false, or b is true. But how to define it?

There are multiple ways, but we define it like this:

imp (a b ∈ prop) := nonempty (⋃ {prop {true → true}}) (a → b)

Explanation: we defined set imp, which is a function that takes two propositions a and b and returns the result of a implies b. Expression (a → b) is a syntactic sugar for (Π (x ∈ a), b). It is the set of all function from the elements of a to the elements of b. If a is false, then for any b there exists a unique function from the elements of a to the elements of b, so the set of all such functions is the set that contains only the empty set, which is definitionally equal to true. If a is true and b is false, the set of all such functions is empty (the result is equal to false).

However, if both a and b are true, there exists a single function from the elements of true to the elements of true (the only element of true is false), but the problem is that such function (which is a set) is not a proposition. We solve that problem by calling nonempty, which converts the given set to a proposition. But, since (true → true) itself is not a proposition, we must parametrize nonempty with propositions plus that additional set. That's why we have nonempty (⋃ {prop {true → true}}). If we just had nonempty prop, then imp true true would be underspecified (because (true → true) ∉ prop).

Another way to define it:

imp (a b ∈ prop) := nonempty {a → b} (a → b)

It is equivalent to the previous definition. Since functions are sets, functional equivalence is extensional.

Next, let's define disjunction and conjunction:

or (a b ∈ prop) := imp (not a) b
and (a b ∈ prop) := not (or (not a) (not b))

Iff and xor:

iff (a b ∈ prop) := and (imp a b) (imp b a)
xor (a b ∈ prop) := not (iff a b)

We can also define the identity function:

id S (a ∈ S) := a

Inspecting sets

Before we proceed to more advanced examples, let's take a look at how the sets (functions) from the Basic examples section look like from inside. Since all those sets are finite, we can inspect them using the #print command:

#print emp           -- {}
#print false         -- {}
#print true          -- {{}}
#print prop          -- {{}, {{}}}
#print is_empty prop -- {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}
#print not           -- {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}
#print nonempty prop -- {{{}, {{}}}, {{{}}, {{{}}}}}
#print imp           -- {{{}, {{}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}
#print or            -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}}
#print and           -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}
#print iff           -- {{{}, {{}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}
#print xor           -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}}}
#print id prop       -- {{{}, {{}}}, {{{}}, {{{}}}}}

We parametrized each proper class with prop for simplicity (we cannot print proper classes).

We can also print more complex constructions like

#print nonempty (id and) -- {{{{{}}, {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}, {{}, {{{}, {{}}}, {{{}}, {{},
                            {{}}}}}}}}}}, {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}, {{}, {{{}, {{}}}, {{{}},
                            {{}, {{}}}}}}}}}}, {{{{}}, {{{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{{}}, {{{}},
                            {{{}, {{}}}, {{{}}, {{{}}}}}}}}}}, {{{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{{}},
                            {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}}}}

which may be hard to comprehend. Note that it is not what it might look like. Set nonempty (id and) is not equal to the result of calling nonempty with the result of calling id with argument and. It is actually a function, which is the result of parametrizing proper class nonempty with the set (id and), while (id and) is the result of parametrizing proper class id with the set and (and is a set, not a proper class). Note the difference:

#print nonempty {id {and} and} (id {and} and) -- {{}}

For convenience, we introduce f! x as a syntactic sugar for f {x} x. The above expression can be written as nonempty! (id! and)

Quantifiers

After defining propositional logic, we can now define the universal and the existential quantifier:

forall S (P ∈ S → prop) := nonempty! (Π (x ∈ S), P x)
exists S (P ∈ S → prop) := not (forall S (λ (x ∈ S), not (P x)))

Here is how they look:

#print forall prop -- {{{{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{{}, {{}}}, {{{}}, {{{}}}}}},
                      {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{},
                      {{}}}}}}, {{{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}

#print exists prop -- {{{{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}},
                      {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{{}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{},
                      {{}}}}}}, {{{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}

The universal quantifier on set $S$ and unary predicate $P$ is true iff there exists a function that maps each element $x\in S$ to an element of proposition $P(x)$. Such function exists iff none of the propositions is false. In other words, the quantifier checks whether $P(x)$ is true for each $x$. That's why we have nonempty - we check whether there exists at least one such mapping.

The existential quantifier is defined using de Morgan laws. We can now define forall' in terms of exists

forall' S (P ∈ S → prop) := not (exists S (λ (x ∈ S), not (P x)))

And, of course, we can print it:

#print forall' prop -- {{{{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{{}, {{}}}, {{{}}, {{{}}}}}},
                       {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{},
                       {{}}}}}}, {{{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}

It is exactly the same as forall. It doesn't matter how we define a function. It only matters what the function does. Consider also this example:

my_func (a ∈ prop) := forall prop (λ (b ∈ prop), imp a b)

What computation does this function perform? Clearly, it is a unary function from prop to prop. But what does it actually do? We can print it:

#print my_func -- {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}

Now, we observe that this is the same output as we get for not, so my_func is equal to not. It actually makes perfect sense: we defined my_func a as a proposition which is true iff a implies any proposition b, which is true iff a is false, so my_func inverts the proposition.

Equality

We define equality using surjection from an unordered pair to prop

surj_prop S := exists (S → prop) λ (P ∈ S → prop),
  and (exists S λ (x ∈ S), P x) (exists S λ (x ∈ S), not (P x))

eq S (x y ∈ S) := not (surj_prop {a, b})

Explanation: Given some set $S$ and two elements $x,y\in S$, we put them in an unordered pair $\left\{x,y\right\}$ and then check whether there exists a surjection from it to prop. If there exists a surjection, it means that $x$ and $y$ are not the same. The existence of a surjection implies that the cardinality of the unordered pair is at least $2$, so if $x$ and $y$ are equal, the pair reduces to only one element.

We can print the equality on propositions:

#print eq prop -- {{{}, {{}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}

As we can see, it is identical to iff. We can also define the not equals operator:

neq S (x y ∈ S) := not (eq S x y)

#print neq prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}}}

Set operations

Union

Union of two sets:

union S (x y ∈ S) := ⋃ {x, y}

Union on props:

#print union prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}}

It is the same as or, so we could define or as:

or (x y ∈ prop) := union prop x y

Remove an element

Remove element $x$ from set $y$:

remove S (x y ∈ S) := {z ∈ y | neq {x, z} x z}

It would be interesting to see what remove does when specialized to propositions:

#print remove prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}

We can clearly see that it is equivalent to and, but why? We can manually check each possible combination:

• remove prop false false - Since false is empty, removing anything from it remains false
• remove prop true false - Ditto
• remove prop false true - Since true contains false as its only element, removing false from true makes true become false
• remove prop true true - true does not contain true, so it remains unchanged

So, we can confirm that this function is equivalent to and when specialized on propositions. But, of course, it can work on any set S.

Set membership

Return true iff $x\in y$:

mem S (x y ∈ S) := neq {remove S x y, y} (remove S x y) y

Set $x$ is a member of set $y$ iff $y$ with $x$ removed is not equal to $y$. If we specialize it on propositions, we get the following result:

#print mem prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}}

It is none of the function we have defined on propositions. So what it actually is? It is a function that returns true iff the first argument is false and the second argument is true. That is the case because (false ∈ true) is true, while it is false for all other combination of propositions.

Intersection

Intersection of two sets:

inter S (x y ∈ S) := {z ∈ x | mem {z, y} z y}

When specialized to props, it is equal to and, as expected.

#print inter prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}

Natural numbers

We can construct the set of the natural numbers, represented as the von Neumann ordinal $\omega$:

0 := emp
nat := {0, λ x, ⋃ {x, {x}}}

It represents the least fixed point. It contains $0$ (which is defined to be the empty set) and whenever it contains set $x$, it also contains $x\cup \left\{x\right\}$.

We cannot print infinite sets:

#print nat -- Segmentation fault (core dumped)

Arithmetic operations

Successor

succ (x ∈ nat) := ⋃ {x, {x}}

Implementation

Implementation in Haskell - It is not an interpreter, but just a small utility for evaluating set expressions.