A new program for combinatory reduction and abstraction

Loading...
Thumbnail Image
Date
2009
Authors
Deshpande, Sushant
University of Lethbridge. Faculty of Arts and Science
Journal Title
Journal ISSN
Volume Title
Publisher
Lethbridge, Alta. : University of Lethbridge, Dept. of Mathematics and Computer Science, c2009
Abstract
Even though lambda calculus (λ-calculus) and combinatory logic (CL) appear to be equivalent, they are not. As yet we do not have a reduction in CL which corresponds to β-reduction in λ-calculus. There are three proposals but they all have few problems one of which is the lack of a complete characterization of CL-terms corresponding to λ-terms in β-normal form. Finding such a characterization for any of the three proposals appears to require a lot of examples which are tedious and time consuming to develop by hand. For this reason, a computer program to do reductions and abstractions of CL-terms would be useful. This thesis is about an attempt to write such a program. The program that we have does not yet work for the three proposals but it works for βη-strong reduction. Coding this program turned out to be much harder than anticipated. Dr. Robin Cockett developed a semantic translation which helped in coding the program but his semantic translation needs to be extended to all three proposals to obtain the program originally desired and that needs a lot of research.
Description
v, 96 leaves ; 29 cm
Keywords
Combinatory logic , Lambda calculus , Dissertations, Academic
Citation