University of Leicester
Browse

On undefined and meaningless in Lambda definability

Download (509.78 kB)
conference contribution
posted on 2016-11-15, 14:35 authored by Fer-Jan De Vries
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.

History

Citation

Leibniz International Proceedings in Informatics, LIPIcs, 2016, 52

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Source

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

Version

  • VoR (Version of Record)

Published in

Leibniz International Proceedings in Informatics

Publisher

Schloss Dagstuhl - Leibniz-Zentrum für Informatik

eissn

1868-8969

isbn

9783959770101

Available date

2016-11-15

Publisher version

http://drops.dagstuhl.de/opus/volltexte/2016/5978/

Notes

1998 ACM Subject Classification F.4.1 [Mathematical Logic] lambda calculus and related systems

Temporal coverage: start date

2016-06-22

Temporal coverage: end date

2016-06-26

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC