Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/38557
Title: On undefined and meaningless in Lambda definability
Authors: De Vries, Fer-Jan
First Published: 22-Jun-2016
Presented at: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Porto, Portugal
Start Date: 22-Jun-2016
End Date: 26-Jun-2016
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Citation: Leibniz International Proceedings in Informatics, LIPIcs, 2016, 52
Abstract: We distinguish between undefined terms as used in lambda definability of partial recursive functions and meaningless terms as used in infinite lambda calculus for the infinitary terms models that generalise the Böhm model. While there are uncountable many known sets of meaningless terms, there are four known sets of undefined terms. Two of these four are sets of meaningless terms. In this paper we first present set of sufficient conditions for a set of lambda terms to serve as set of undefined terms in lambda definability of partial functions. The four known sets of undefined terms satisfy these conditions. Next we locate the smallest set of meaningless terms satisfying these conditions. This set sits very low in the lattice of all sets of meaningless terms. Any larger set of meaningless terms than this smallest set is a set of undefined terms. Thus we find uncountably many new sets of undefined terms. As an unexpected bonus of our careful analysis of lambda definability we obtain a natural modification, strict lambda-definability, which allows for a Barendregt style of proof in which the representation of composition is truly the composition of representations.
DOI Link: 10.4230/LIPIcs.FSCD.2016.18
ISBN: 9783959770101
eISSN: 1868-8969
Links: http://drops.dagstuhl.de/opus/volltexte/2016/5978/
http://hdl.handle.net/2381/38557
Version: Publisher Version
Status: Peer-reviewed
Type: Conference Paper
Rights: © Fer-Jan de Vries; licensed under Creative Commons License CC-BY
Description: 1998 ACM Subject Classification F.4.1 [Mathematical Logic] lambda calculus and related systems
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
LIPIcs-FSCD-2016-18.pdfPublished (publisher PDF)509.78 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.