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