(* Translated from Example 7 in Schuermann, Poswolsky, and Sarnat's
2004 technical report on the nabla-calculus. *)
(* By the way, the algorithm is quadratic in complexity. I don't
know if there exists a better algorithm, although I would imagine
so. *)
type comb =
| V of atom
| K
| S
| MP of comb * comb
type term =
| Var of atom
| Lam of < atom * inner term >
| App of term * term
fun ba accepts x, c produces d
where free(d) <= free(c) \ free(x)
=
case c of
| V (y) ->
if x == y then
MP (MP (S, K), K)
else
MP (K, V (y))
end
| K ->
MP (K, K)
| S ->
MP (K, S)
| MP (c1, c2) ->
MP (MP (S, ba (x, c1)), ba (x, c2))
end
fun convert accepts t produces c =
case t of
| Var (x) ->
V (x)
| App (t1, t2) ->
MP (convert (t1), convert (t2))
| Lam (x, t) ->
ba (x, convert (t))
end
(* Some readers may be dissatisfied by the fact that the type of
combinators includes a V case for variables. Let's move to a type
that doesn't. We don't have to do this -- because knowing that the
support of a combinator is empty is sufficient to ensure that the V
case cannot arise -- but we can -- for the same reason. *)
type closed_comb =
| CK
| CS
| CMP of closed_comb * closed_comb
fun ground accepts c
where free(c) == empty
produces cclosed
=
case c of
| V (_) ->
absurd (* this is a static check *)
| K ->
CK
| S ->
CS
| MP (c1, c2) ->
CMP (ground (c1), ground (c2))
end
fun convert_closed accepts t
where free(t) == empty
produces cclosed
=
ground (convert (t))