Demo of the ShotUn Package

Copy Markdown View Source
Run in Livebook 
Mix.install([
  {:shot_un, path: Path.expand("..", __DIR__)},
  {:kino, "~> 0.19"}
])

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(&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.

Visualization: the decision tree of pre-unification

Every public entry point of ShotUn accepts a vis: true option. When set, the call returns a {result, %ShotUn.Trace{}} tuple instead of a bare result. The trace is a tree of ShotUn.Trace.Node records covering only the paths from the initial state to a solution leaf — failed branches and dead-end intermediate steps are pruned out. ShotUn.Trace.Mermaid.render/2 produces a Mermaid graph TD string that we can render inline with Kino.Mermaid.new/1.

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

{stream, trace} = unify({x, c}, 10, vis: true)
Enum.to_list(stream) |> Enum.map(&Kernel.to_string/1) |> IO.puts
trace |> ShotUn.Trace.Mermaid.render() |> Kino.Mermaid.new()

For the simple $X \overset{?}{=} c$ problem the trace is a linear chain init -.-> bind -.-> solution. Dotted arrows mark linear continuations.

Visualization: branching on imitation and projection

The flex-rigid problem $X~a~a \overset{?}{=} f~a~a$ revisits the nine-solution example. The top-level projections substitute $X$ by $\lambda \lambda.~1$ or $\lambda \lambda.~2$, both collapsing the equation to $a \overset{?}{=} f~a~a$ which is a rigid clash; those branches are pruned. Only the imitation $X \leftarrow \lambda \lambda.~f~H_1~H_2$ survives, and each $H_i$ then branches three ways (imitation through $a$, projection onto either argument), producing the 3 × 3 = 9 solution leaves visible in the diagram. Branching choice points use solid arrows (==>); linear continuations use dotted arrows (-.->).

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())

{_stream, trace} = unify({app(x, [a, a]), app(f, [a, a])}, 10, vis: true)

trace |> ShotUn.Trace.Mermaid.render() |> Kino.Mermaid.new()

Visualization: pattern unification and second-order matching

ShotUn.pattern_unify/2 and ShotUn.match/2 accept the same vis: true option. Pattern unification is a single-path work-list rewrite, so its trace is a linear chain — useful to inspect the inversion, alias and intersection rules in action. Below, the flex-flex pair $X \overset{?}{=} Y$ resolves via the intersection rule by binding both $X$ and $Y$ to a fresh meta variable.

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

{{:ok, sol}, trace} = pattern_unify({x, y}, vis: true)
IO.puts(Kernel.to_string(sol))

trace |> ShotUn.Trace.Mermaid.render() |> Kino.Mermaid.new()

Second-order matching enumerates all matchers; the trace shows the full set of branches that reached a solution, side by side. The example below — matching $X~a~a$ against the ground target $f~a~a$ — yields the same nine matchers, but here each branch terminates immediately because the target is already ground.

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())

{_stream, trace} = match({app(x, [a, a]), app(f, [a, a])}, vis: true)

trace |> ShotUn.Trace.Mermaid.render() |> Kino.Mermaid.new()