From λ-terms to combinators for α-spine

Proof-of-concept code for compiling a λ-term M into a pair (t_M,👁_M) of a term t_M and an Applicative Inductive Interaction system (pronounced as aye / eye) 👁_M, with M and t_M having isomorphic reduction graphs under α-spine β-reduction respectively 👁_M-reduction. Concept proven is that compilation is linear in M.