de Vries, FerJan
On Undefined and Meaningless in Lambda Definability
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 Bohm 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 lambdadefinability, which
allows for a Barendregt style of proof in which the representation of
composition is truly the composition of representations.
BibTeX  Entry
@InProceedings{devries:LIPIcs:2016:5978,
author = {FerJan de Vries},
title = {{On Undefined and Meaningless in Lambda Definability}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {18:118:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770101},
ISSN = {18688969},
year = {2016},
volume = {52},
editor = {Delia Kesner and Brigitte Pientka},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/5978},
URN = {urn:nbn:de:0030drops59785},
doi = {10.4230/LIPIcs.FSCD.2016.18},
annote = {Keywords: lambda calculus, lambda definability, partial recursive function, undefined term, meaningless term}
}
2016
Keywords: 

lambda calculus, lambda definability, partial recursive function, undefined term, meaningless term 
Seminar: 

1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Issue date: 

2016 
Date of publication: 

2016 