抽象算法C-T-ABS和ABSTRACT的理论推导与等价性证明

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

摘要: ABSTRACT,C-T-ABS 是把λ表达式转换成SKI 表达式的抽象算法,是函数式语言实现的理论基础。本文从λ演算、SKI 演算的基本理论出发,对这两个算法进行了理论推导及功能上的等价性证明。展示了对同一输入,C-T-ABS 能生成较优化的代码,并对它们生成代码的长度及归约效率进行了比较。

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.