ABSTRACT. We introduce, in a general setting, an “analytic” version of standard equational calculi of combinatory logic. Analyticity lies on the one side in the fact that these calculi are characterized by the presence of combinatory introduction rules in place of combinatory axioms, and on the other side in that the transitivity rule proves to be eliminable. Apart from consistency, which follows immediately, we discuss other almost direct consequences of analyticity and the main transitivity elimination theorem; in particular the Church-Rosser and the leftmost reduction theorems for the associated notions of reduction. The last two sections deal with analytic combinatory calculi with the extensionality rule added. Here, as far as the elimination of transitivity is concerned, we have only partial results, which unfortunately do not cover, at present, full CL+Ext. Yet, they are sufficient to prove the decidability of weaker combinatory calculi with extensionality, including e.g. BCK + Ext.
Analytic combinatory calculi and the elimination of transitivity / P. MINARI. - In: ARCHIVE FOR MATHEMATICAL LOGIC. - ISSN 0933-5846. - STAMPA. - 43:(2004), pp. 159-191. [10.1007/s00153-003-0203-1]
Analytic combinatory calculi and the elimination of transitivity
MINARI, PIERLUIGI
2004
Abstract
ABSTRACT. We introduce, in a general setting, an “analytic” version of standard equational calculi of combinatory logic. Analyticity lies on the one side in the fact that these calculi are characterized by the presence of combinatory introduction rules in place of combinatory axioms, and on the other side in that the transitivity rule proves to be eliminable. Apart from consistency, which follows immediately, we discuss other almost direct consequences of analyticity and the main transitivity elimination theorem; in particular the Church-Rosser and the leftmost reduction theorems for the associated notions of reduction. The last two sections deal with analytic combinatory calculi with the extensionality rule added. Here, as far as the elimination of transitivity is concerned, we have only partial results, which unfortunately do not cover, at present, full CL+Ext. Yet, they are sufficient to prove the decidability of weaker combinatory calculi with extensionality, including e.g. BCK + Ext.File | Dimensione | Formato | |
---|---|---|---|
AML2004.pdf
Accesso chiuso
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
Tutti i diritti riservati
Dimensione
316.05 kB
Formato
Adobe PDF
|
316.05 kB | Adobe PDF | Richiedi una copia |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.