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. / v, 96 leaves ; 29 cm
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:ALU.w.uleth.ca/dspace#10133/1296 |
| Date | January 2009 |
| Creators | Deshpande, Sushant, University of Lethbridge. Faculty of Arts and Science |
| Contributors | Seldin, Jonathan |
| Publisher | Lethbridge, Alta. : University of Lethbridge, Dept. of Mathematics and Computer Science, c2009, Arts and Science, Department of Mathematics and Computer Science |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | en_US |
| Detected Language | English |
| Type | Thesis |
| Relation | Thesis (University of Lethbridge. Faculty of Arts and Science) |
Page generated in 0.0024 seconds