CINNI - A Calculus of Indexed Names and Named Indices

Mark-Oliver Stehr

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:

  1. Mark-Oliver Stehr: CINNI - A New Calculus of Explicit Substitutions and its Application to Pure Type Systems, Manuscript, CSL, SRI-International, Menlo Park, CA, USA, May 1999
  2. Mark-Oliver Stehr, Jose Meseguer: Pure Type Systems in Rewriting Logic , Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999. Paper available here . Extended version submitted for publication.
  3. Mark-Oliver Stehr: CINNI - A Generic Calculus of Explicit Substitutions and its Application to lambda-, sigma- and pi-calculi , Third International Workshop on Rewriting Logic and its Applications (WRLA'2000), Kanazawa, Japan, September 18 - 20, 2000, Electronic Notes in Theoretical Computer Science, Elsevier, 2000 ( ENTCS Link , extended version available)