Demo of the ShotUn Package

Mix.install([
  {:shot_un, "~> 0.1.0"}
])

Setup

ShotDs defines various data structures for HOL

import ShotDs.Hol.Dsl
import ShotDs.Hol.Definitions
import ShotDs.Stt.Numerals
import ShotDs.Util.Formatter
alias ShotDs.Data.Type
alias ShotDs.Stt.TermFactory, as: TF

import ShotUn

Example: Church Numerals

In simple type theory, church numerals are defined as lambda terms accepting a successor function $s{\iota\to\iota}$ and a _starting point $z_\iota$ which return the $n$-fold application of $s$ to $z$. E.g., the numeral for $0$ is $\lambda s z. z$, for $1$ $\lambda s z. s z$, for $2$ $\lambda s z. s (s z)$ and so on.

Based on this encoding, we can define some basic operations on natural numbers as follows:

$$\mathrm{succ}~n \coloneqq \lambda s~z.~s~(n~s~z)$$ (apply the successor function to $n$)

$$\mathrm{plus}~m~n \coloneqq \lambda s~z.~m~s~(n~s~z)$$ (apply the successor function $m$ times to $n$)

$$\mathrm{mult}~m~n \coloneqq \lambda s~z.~m~(n~s)~z$$ (apply $(\mathrm{plus}~n)$ $m$ times)

Note that more complex functions like exponentiation or difference are not expressible without polymorphic types.

for n <- 0..10, do: "#{n} := #{format!(num(n))}"
|> IO.puts

Example: X ∙ 5 =? 30

x_times_5 = mult(num_var("X"), num(5))

unify({x_times_5, num(30)}) |> Enum.map(&Kernel.to_string/1) |> IO.puts

The algorithm finds a solution by substituting $X$ by the Church encoding of $6$.

Note that the unification algorithm returns a Stream which can be used like any other enumerable. Solutions are computed lazily.

Example: X ∙ 10 =? 1000

x_times_10 = mult(num_var("X"), num(10))

unify({x_times_10, num(1000)}, 1000) |> Enum.map(&Kernel.to_string/1) |> IO.puts

The algorithm finds a solution by substituting $X$ by the Church encoding of $100$.

Example: X ∙ Y =? 4

x_times_y = mult(num_var("X"), num_var("Y"))

unify({x_times_y, num(4)})
|> Enum.map(&Kernel.to_string/1) |> Enum.join("\n") |> IO.puts

The algorithm finds three solutions to the problem:

• substituting $Y$ by the Church encoding of $4$ and $X$ by the encoding of $1$
• substituting $Y$ and $X$ by the Church encoding of $2$
• substituting $Y$ by the Church encoding of $1$ and $X$ by the encoding of $4$

Example: X a a =? f a a

x = TF.make_free_var_term("X", type_iii())
f = TF.make_const_term("f", type_iii())
a = TF.make_const_term("a", type_i())

unify({app(x, [a, a]), app(f, [a, a])})
|> Enum.map(&Kernel.to_string/1) |> Enum.join("\n") |> IO.puts

The algorithm finds nine total solutions which correspond to all combinations of projections and imitations:

• $\lambda\lambda.~f~a~a~/~X$
• $\lambda\lambda.~f~a~2~/~X$
• $\lambda\lambda.~f~a~1~/~X$
• $\lambda\lambda.~f~2~a~/~X$
• $\lambda\lambda.~f~2~2~/~X$
• $\lambda\lambda.~f~2~1~/~X$
• $\lambda\lambda.~f~1~a~/~X$
• $\lambda\lambda.~f~1~2~/~X$
• $\lambda\lambda.~f~1~1~/~X$

Example: X (f a) =? f (X a)

x = TF.make_free_var_term("X", type_ii())
f = TF.make_const_term("f", type_ii())
a = TF.make_const_term("a", type_i())

unify({app(x, app(f, a)), app(f, app(x, a))}, _depth=5)
|> Enum.map(&Kernel.to_string/1) |> Enum.join("\n") |> IO.puts

The algorithm finds four solutions to the problem at the given depth of 5. Other solutions can be found when increasing this depth limit. We see that the solutions for this problem follow the pattern of substituting $X$ by the $n$-fold composition of $f$ ($n \in [0, 4]$ for depth 5).

Example: System of Equations

(1) $(x\cdot y) + z = 21$

(2) $x + y + z = 10$

(3) $(x \cdot z) + y = 9$

[x, y, z] = for n <- ["X", "Y", "Z"], do: num_var(n)

eqs = [
  {plus(mult(x, y), z), num(21)},
  {plus(plus(x, y), z), num(10)},
  {plus(mult(x, z), y), num(9)}
]

unify(eqs, 50)
|> Enum.map(&amp;Kernel.to_string/1) |> Enum.join("\n") |> IO.puts

The algorithm finds two solutions for the given problem with depth 50:

• substituting $Z$ by the Church encoding of $1$, $Y$ by the encoding of $5$ and $X$ by the encoding of $4$
• substituting $Z$ by the Church encoding of $1$, $Y$ by the encoding of $4$ and $X$ by the encoding of $5$

Note that in this case, increasing the depth limit does not yield more solutions even though some unification branches are incomplete.

Example: X =? Y c

x = TF.make_free_var_term("X", type_i())
y = TF.make_free_var_term("Y", type_ii())
c = TF.make_const_term("c", type_i())

unify({x, app(y, c)})
|> Enum.map(&Kernel.to_string/1) |> IO.puts

$X \overset{?}{=} Y~c$ is an example for the flex-flex case. For these cases, often infinite solutions exist. To ensure semi-decidability, unification is deferred and a list of flex-flex pairs is returned as future constraints.