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

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

作　　者：杨祥金[1] 

机构地区：[1]东南大学计算机系,南京210018

出　　处：《计算机研究与发展》1993年第12期1-11,共11页Journal of Computer Research and Development

基　　金：国家自然科学基金DDFP

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

关 键 词：抽象算法 Λ演算 SKI演算 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]