Tutorial 9: Determinism vs Non Determinism

In the last tutorial, you learned about tunnels, holes and spheres.

Now, it is time to talk about determinism vs non-determinism.

Determinism means that you get the same output each time you call a function with the same inputs as before.

Non-determinism means that you might get different outputs for same inputs.

This tutorial will contain more technical details, in order to define precisely what determinism and non-determinism means, without having direct access to a random source.

If you like to, then you can skip these details and read the summary.

Points are deterministic functions

A point f : A -> B has the property that every input x : A only has one output f(x) : B:

f : A -> B  where ∀ x : A { |∃f{(= x)}| == 1 }

Here, |∃f{(= x)}| counts the number of output values:

|∃f{(= x)}| = ∑ y : B { if (∃f{(= x)})(y) { 1 } else { 0 } }

The expression f{(= x)} filters the input such that only values equal to x passes through, and ∃f{(= x)} finds a function such that for every filtered output of f, it returns true and false otherwise. The reason f(x) is not used directly, is that for non-deterministic functions this is not reliable.

∃f{(= x)} : B -> bool

In general, one uses ∀f to talk about inputs of f (domain) and ∃f to talk about outputs of f (codomain). In Path Semantics the domain can also be referred to as "the trivial path" and the codomain as "the existential path". The reason Path Semantics has these names, instead of just using domain and codomain, is that these ideas can be generalized, such as "the probabilistic existential path".

In general, the existential path is undecidable, meaning there is no algorithm that can automatically derive it for all functions.

A simple kind of point is a function of type f : () -> T, which might be thought of as a constant.

Points have the characteristic that they are pure functions and hence deterministic.

In some cases, a deterministic function might be thought of as a path or homotopy. This means, the term "point" can be used relatively. Therefore, it makes no sense to say that all deterministic functions are points.

Non-deterministic functions are holes

In general, a non-deterministic function can be defined as:

f : A -> B  where !∀ x : A { |∃f{(= x)}| == 1 }

However, using this definition can be difficult e.g. when reasoning about holes.

Now, imagine a function f:

f : A -> B  where |A| < |B|

This function can still be a point, because it is not necessary to cover the whole type of B.

To express a non-deterministic function using this idea, I need a stronger statement:

f : A -> B  where |∀f| < |∃f|

Here, |∀f| (number of inputs) counts the domain of f and |∃f| (number of outputs) counts the codomain of f.

Since there are more outputs than inputs, there must be at least one input that maps to two different outputs.

Let us apply this to a hole (a normal path with no solution):

f[g] : A -> B  where |∀f[g]| < |∃f[g]|

For example:

∵ add : nat x nat -> nat
∵ add[even x even -> id]  where |∀add[even x even -> id]| < |∃add[even x even -> id]|
∴ add[even x even -> id]  where |bool x bool| < |\(_ : nat) = true|
∴ add[even x even -> id]  where |4| < |nat|
∴ add[even x even -> id]

The constraint |∀add[even x even -> id]| < |∃add[even x even -> id]| is automatically satisfied, because one can derive these properties from the normal path directly.

However, we do not know whether it is possible to define add[even x even -> id].

One way to interpret this scenario, is that holes must be non-deterministic if they are implemented.

An example of a simple hole that is non-deterministic, is:

random : () -> real

This function returns a random real number in the unit interval.

In general, it makes no sense to say that all holes are non-deterministic functions, but it is possible to create a language with a such property, by implementing all holes.

Summary

• f{c} filters inputs of f by c
• ∀f are the inputs of f
• ∃f are the outputs of f
• |f| counts values satisfying f
• Points are deterministic functions
• Non-deterministic functions are holes