© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Unlimp - uniqueness as a leitmotiv for implementation
Stefan Kahrs
In Maurice Bruynooghe and Martin Wirsing, editors, Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 182-196. Springer, August 1992.Abstract
When evaluation in functional programming languages is explained using $\lambda$-calculus and/or term rewriting systems, expressions and function definitions are often defined as terms, that is as {\em trees}. Similarly, the collection of all terms is defined as a {\em forest}, that is a directed, acyclic graph where every vertex has at most one incoming edge. Concrete implementations usually drop the last restriction (and sometimes acyclicity as well), i.e.\ many terms can share a common subterm, meaning that different paths of subterm edges reach the same vertex in the graph.
Any vertex in such a graph represents a term. A term is represented uniquely in such a graph if there are no two different vertices representing it. Such a representation can be established by using {\em hash-consing} for the creation of heap objects. We investigate the consequences of adopting uniqueness in this sense as a leitmotiv for implementation (called Unlimp), i.e.\ not {\em allowing} any two different vertices in a graph to represent the same term.
Download publication 76 kbytes
Bibtex Record
@conference{575,
author = {Stefan Kahrs},
title = {Unlimp -- uniqueness as a leitmotiv for implementation},
month = {August},
year = {1992},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1992/575},
booktitle = {Programming Language Implementation and Logic Programming},
editor = {Maurice Bruynooghe and Martin Wirsing},
publisher = {Springer},
refereed = {yes},
series = {Lecture Notes in Computer Science},
volume = {631},
}