License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2011.458
URN: urn:nbn:de:0030-drops-32493
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3249/
Go to the corresponding LIPIcs Volume Portal

Polonsky, Andrew

Axiomatizing the Quote

pdf-format:
36.pdf (0.5 MB)

Abstract

We study reflection in the Lambda Calculus from an axiomatic point of view. Specifically, we consider various properties that the quote operator must satisfy as a function on lambda terms. The most important of these is the existence of a definable left inverse, a so-called evaluator for the quote operator. Usually the quote operator encodes the syntax of a given term, and the evaluator proceeds by analyzing the syntax and reifying all constructors by their actual meaning in the calculus. Working in Combinatory Logic, Raymond Smullyan (1994) investigated which elements of the syntax must be accessible via the quote in order for an evaluator to exist. He asked three specific questions, to which we provide negative answers. On the positive side, we give a characterization of quotes which possess all of the desired properties, equivalently defined as being equitranslatable with a standard quote. As an application, we show that Scott's coding is not complete in this sense, but can be slightly modified to be such. This results in a minimal definition of a complete quoting for Combinatory Logic.

BibTeX - Entry

@InProceedings{polonsky:LIPIcs:2011:3249,
  author =	{Andrew Polonsky},
  title =	{{Axiomatizing the Quote}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{458--469},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3249},
  URN =		{urn:nbn:de:0030-drops-32493},
  doi =		{10.4230/LIPIcs.CSL.2011.458},
  annote =	{Keywords: lambda calculus, combinatory logic, quote operator, enumerator}
}

Keywords: lambda calculus, combinatory logic, quote operator, enumerator
Collection: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue Date: 2011
Date of publication: 31.08.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI