Keywords: Names, Explicit Substitutions, Bound Variables, Higher-Order Calculi, Lambda Calculus, Object Calculus, Type Systems
The Calculus of Indexed Names and Named Indices (CINNI) is a new calculus of explicit substitutions that combines names and indices in a uniform way. It contains the standard named notation used in logics and programming languages as well as de'Bruijn's indexed notation as sublanguages. CINNI is a first-order calculus of extreme simplicity that can serve as a generic basis for representing and implementing higher-order languages in a first-order framework. More precisely, CINNI should not be regarded as a single calculus but merely as a family of calculi that is parameterized by syntax of the language to be represented.
We think that CINNI is a suitable basis to deal with the problem of binding and substitution in implementations of logics and other languages, in particular those of higher-order nature. A distinctive advantage of CINNI is that it completely eliminates the problematic translation between the notation that is visible by the user of a system and the internal representation.
As concrete examples we have studied the application of CINNI to the untyped lambda calculus, the object calculus (introduced by Cardelli and Abadi) and to a rich class of typed lambda calculi, namely pure type systems, and, last but not least the proof assistant for OCC, the open calculus of constructions, makes essential use of CINNI. Since CINNI is a calculus that has an executable semantics in terms of rewriting we have indeed obtained with very moderate effort representations of these formalisms that can be executed using the Maude engine.
Relevant References: