# Unification Examples

```elixir
Mix.install([{:hol, "1.0.1"}])
```

## Setup

```elixir
import HOL.Data
import HOL.Terms
import HOL.ChurchNumerals
import HOL.Unification
import PrettyPrint

LoggerHelper.set_logger_warning()
```

Here we setup the types we need to construct the following examples

```elixir
type_i = mk_type(:i)
type_ii = mk_type(type_i, [type_i])
type_ii_ii = mk_type(type_ii, [type_ii])
type_iii = mk_type(type_i, [type_i, type_i])
```

## Example: x \* 5 = 30

```elixir
t_x = mk_free_var_term("x", type_ii_ii)

x_times_5 = mult_term() |> mk_appl_term(t_x) |> mk_appl_term(mk_num(5))
input = {x_times_5, mk_num(30)}

result = unify(input)
pp_res(result, true)
```

This finds one substitution that replaces `x` with the church numeral `6`

x = 6: `x <- λ 2 1. 2 (2 (2 (2 (2 (2 1)))))`

## Example: x \* 10 = 1000

```elixir
t_x = mk_free_var_term("x", type_ii_ii)

x_times_10 = mult_term() |> mk_appl_term(t_x) |> mk_appl_term(mk_num(10))

input = [
  {x_times_10, mk_num(1000)}
]

result = unify(input, true, 1000)
pp_res(result, true)
```

This finds one substitution that replaces `x` with the church numeral `100`

x = 100: `x <- (2 1. 2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )`

## Example: x \* y = 4

```elixir
t_x = mk_free_var_term("x", type_ii_ii)
t_y = mk_free_var_term("y", type_ii_ii)

x_times_y = mult_term() |> mk_appl_term(t_x) |> mk_appl_term(t_y)
input = {x_times_y, mk_num(4)}

result = unify(input, true, 40)
pp_res(result, true)

# 1*4=4 & 4*1=4 & 2*2=4
```

This finds three solutions:

y = 1, x = 4: `y <- λ 2 1. 2 1` | `x <- λ 2 1. 2 (2 (2 (2 1)))`

y = 2, x = 2: `y <- λ 2 1. 2 (2 1)` | `x <- λ 2 1. 2 (2 1)`

y = 4, x = 1: `y <- λ 2 1. 2 (2 (2 (2 1)))` | `x <- λ 2 1. 2 1`

## Example: xaa = faa

```elixir
t_x = mk_free_var_term("x", type_iii)
t_a = mk_const_term("a", type_i)
t_f = mk_const_term("f", type_iii)

xaa = mk_appl_term(mk_appl_term(t_x, t_a), t_a)
faa = mk_appl_term(mk_appl_term(t_f, t_a), t_a)

input = {xaa, faa}

result = unify(input)
pp_res(result)
```

Finds nine possible substitutions for unification:

`x <- λ 2 1. f 1 1`

`x <- λ 2 1. f 1 2`

`x <- λ 2 1. f 1 a`

`x <- λ 2 1. f 2 1`

`x <- λ 2 1. f 2 2`

`x <- λ 2 1. f 2 a`

`x <- λ 2 1. f a 1`

`x <- λ 2 1. f a 2`

`x <- λ 2 1. f a a`

## Example: x(fa) = f(xa)

```elixir
t_x = mk_free_var_term("x", type_ii)
t_f = mk_const_term("f", type_ii)
t_a = mk_const_term("a", type_i)

xfa = mk_appl_term(t_x, mk_appl_term(t_f, t_a))
fxa = mk_appl_term(t_f, mk_appl_term(t_x, t_a))

depth = 5
input = {xfa, fxa}

result = unify(input, true, depth)
pp_res(result)
```

This finds four solutions:

`x <- λ 1. 1 `

`x <- λ 1. f 1`

`x <- λ 1. f (f 1)`

`x <- λ 1. f (f (f 1))`

However the maximum search depth was also reached twice. This means that it might not have found all solutions. Try changing the `depth` value and see what other solutions can be found!

## Example: Multiple Equations

- xy+z=21
- x+y+z=10
- xz+y=9

```elixir
t_x = mk_free_var_term("x", type_ii_ii)
t_y = mk_free_var_term("y", type_ii_ii)
t_z = mk_free_var_term("z", type_ii_ii)

input = [
  {plus(mult(t_x, t_y), t_z), mk_num(21)},
  {plus(plus(t_x, t_y), t_z), mk_num(10)},
  {plus(mult(t_x, t_z), t_y), mk_num(9)}
]

depth = 50
result = unify(input, true, depth)
pp_res(result, true)
```

Two Solutions are found here:

z = 1, y = 4, x = 5: `z <- λ 2 1. 2 1` | `y <- λ 2 1. 2 (2 (2 (2 1)))` | `x <- λ 2 1. 2 (2 (2 (2 (2 1))))`

z = 1, y = 5, x = 4: `z <- λ 2 1. 2 1` | `y <- λ 2 1. 2 (2 (2 (2 (2 1))))` | `x <- λ 2 1. 2 (2 (2 (2 1)))`

Once again the maximum search depth was reached multiple times. However increasing the search depth will not yield more solutions here. Unification doesn't always terminate even when no more solutions can be found!

## Example: x = zc

```elixir
t_x = mk_free_var_term("x", type_i)
t_z = mk_free_var_term("z", type_ii)
t_c = mk_const_term("c", type_i)
appl_zc = mk_appl_term(t_z, t_c)

input = {t_x, appl_zc}
result = unify(input)
pp_res(result)
```

Here the only given result is the tuple `{x,(z c)}` on the flexlist. The tuples on the flexlist are not resolved, since this algorithm only does pre-unification. Many (often infinite) substitutions can be created from these tuples. This functionality is not currently present in this module.