2015/08/31 by Mayer Goldberg
Computer Science · Mathematics · #Algebra over a field #Arity #Combinatory logic #Computability, Logic, AI Algorithms #Computer science #Discrete mathematics #Fixed point #Generalization #Logic, programming, and type systems #Mathematics #Modulo #Numerical Methods and Algorithms #Programming language #Pure mathematics #Variable (mathematics) #cs.LO
paper · pdf · doi:10.2168/lmcs-11(3:25)2015
published in Logical Methods in Computer Science Volume 11, Issue 3 (Logical Methods in Computer Science e.V.) · 31 pages
arxiv created 2015/09/30 · openalex publication_date 2015/10/01 · arxiv updated 2017/01/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
Ellipses are a meta-linguistic notation for denoting terms the size of which are specified by a meta-variable that ranges over the natural numbers. In this work, we present a systematic approach for encoding such meta-expressions in the \I-calculus, without ellipses: Terms that are parameterized by meta-variables are replaced with corresponding \I-abstractions over actual variables. We call such \I-terms arity-generic. Concrete terms, for particular choices of the parameterizing variable are obtained by applying an arity-generic \I-term to the corresponding numeral, obviating the need to use ellipses. For example, to find the multiple fixed points of n equations, n different \I-terms are needed, every one of which is indexed by two meta-variables, and defined using three levels of ellipses. A single arity-generic \I-abstraction that takes two Church numerals, one for the number of fixed-point equations, and one for their arity, replaces all these multiple fixed-point combinators. We show how to define arity-generic generalizations of two historical fixed-point combinators, the first by Curry, and the second by Turing, for defining multiple fixed points. These historical fixed-point combinators are related by a construction due to B\~Ahm: We show that likewise, their arity-generic generalizations are related by an arity-generic generalization of B\~Ahm's construction. We further demonstrate this approach to arity-generic \I-definability with additional \I-terms that create, project, extend, reverse, and map over ordered n-tuples, as well as an arity-generic generator for one-point bases.