Theoretical Derivation and Equivalent Proof of Abstractive Algorithm C-T-ABS and Abstract

C-T-ABS abstractive algorithm transforms λ-expression to SKI-expression,which is the theoretical foundation of functional programming language implementation.This paper presents the derivation of two algorithms from λ-calculus and SKI-calculus and gives equivalent proof in power.The generative codes from C-T-ABS are better than ABSTRACT for the same input and the length of generated code and the reductive effect are compared.