[Prev][Next][Index][Thread]

A New Basic Set or Proof Transformations



A New Basic Set of Transformations between Proofs
(Abstract)
(Submitted for presentation at Logic Colloquium '95, August 9-17, Haifa, Israel)

Deductive systems based on the so-called Curry-Howard isomorphism [How80] have
an interesting feature: normalization and strong normalization (Church-Rosser
property) theorems can be proved by reductions on the terms of the functional
calculus.  Exploring this important characteristic, we have proved these
theorems for the Labelled Natural Deduction (LND) [deQGab92] via a term
rewriting system (TRS) constructed from the LND-terms of the functional calculus
[deOldeQ94,deOldeQ95].  The LND system is an instance of Gabbay's Labelled
Deductive Systems (LDS) [Gab94], which is based on a generalization of the
functional interpretation of logical connectives [GabdeQ92] (i.e. Curry-Howard
isomorphism).

Proving the `termination' and `confluence' properties for the TRS associated to
the LND system (TRS-LND) [deOldeQ94], we have in fact proved the normalization
and strong normalization theorems for the LND system, respectively.  The
`termination' property guarantees the existence of a normal form of the
LND-terms, while the `confluence' property its uniqueness.  Thus, because of the
Curry-Howard isomorphism, we have that every LND derivation converts to a normal
form (normalization theorem) and it is unique (strong normalization theorem)
[deOl95,deOldeQ95].

The significance of applying this technique in the proof of the normalization
theorems lies in the presentation of a simple and computational method, which
allowed the discovery of a new basic set of transformations between proofs,
which we baptized as `$\iota$ (iota)-reductions' [deOl95]. With this result, we
obtained a confluent system which contains the $\eta$-reductions.
Traditionally, $\eta$-reductions have not been given an adequate status, as
rightly pointed out by Girard in [Gir89, p. 16], when he defines the `primary'
equations, which correspond to $\beta$-equations, and the `secondary' equations,
which are $\eta$-equations. Girard [Gir89] says that the system given by these
equations is consistent and decidable, however he notes the following:

	``Although this result holds for the whole set of equations, one only
	ever considers the first three. It is a consequence of the
	{\em Church-Rosser property} and the {\em normalization theorem}.''

The first three equations, referred to by Girard, are the `primary' ones,
i.e. $\beta$-equations. 

Applying the so-called `completion procedure', proposed by Knuth and Bendix in
[KnuB70], to TRS-LND, the following term, which causes a non-confluence in the
system, is produced (i.e. a divergent critical pair is generated):

          w(CASE(c,\upsilon{x}.inl(x),\upsilon{y}.inr(y)))

This term rewrites in two different ways (see note (*) at the end of this
text):

1. \leadsto_\eta   w(c)
2. \leadsto_\zeta  CASE(c,\upsilon{x}.w(inl(x)),\upsilon{y}.w(inr(y)))

The method of Knuth and Bendix says that when a terminating system is not
confluent it is possible to add rules in such a way that the resulting system
becomes confluent.  Thus, applying this procedure to TRS-LND, a new rule is
added to the system:

   CASE(c,\upsilon{x}.w(inl(x)),\upsilon{y}.w(inr(y))) \leadsto_\iota w(c)

Since terms represent proof-constructions in the LND system, this rule defines
a new transformation between proofs:

$\iota$-reduction-$\lor$

                      [x:A]             [y:B]
                   --------------    --------------
                   inl(x):A\lor B    inr(y):A\lor B
                   -------------(r)  -------------(r)
  c:A\or B          w(inl(x)):W       w(inr(y)):W
  -----------------------------------------------------($\lor$-elim)
  CASE(c,\upsilon{x}.w(inl(x)),\upsilon{y}.w(inr(y))):W


                  \leadsto_\iota


                    c:A\lor B
                   -----------(r)
                     w(c):W

Similarly, the $\iota$-reduction for the existential quantifier is defined
[deOl95], since, similarly to $\lor$, the quantifier $\exists$ is a
`Skolem-type' operator (i.e. in the `elimination' inference for this type of
operator is necessary to open local assumptions):

$\iota$-reduction-$\exists$

                              [t:D]        [g(t):P(t)]
                        ----------------------------------------($\exists$-intr)
                        \varepsilon{y}.(g(y),t):\exists{y^D}.P(y)
                        -----------------------------------------(r)
 c:\exists{x^D}.P(x)          w(\varepsilon{y}.(g(y),t)):W
 --------------------------------------------------------------($\exists$-elim)
    INST(c,\sigma{g}.\sigma{t}.w(\varepsilon{y}.(g(y),t))):W



                     \leadsto_\iota



                   c:\exists{x^D}.P(x)
                   -------------------(r)
                         w(c):W


(where `$\varepsilon$' is an abstractor).

With this result, we believe that we have offered one possible answer to the
question as to why $\eta$-reductions are not usually considered in the proofs of
the normalization theorems (`confluence' requires $\iota$-reductions).  However,
by applying a computational and well-defined method, the completion procedure,
it seems that this problem of the non-confluence caused by $\eta$-reductions are
solved. 

REFERENCES

[deOl95]
Anjolina Grisi de Oliveira.
Proof Transformations for Labelled Natural Deduction via Term Rewriting.
(In Portuguese).
Master's thesis, Depto. de Inform\'{a}tica, Universidade Federal de
Pernambuco (UFPE), C.P. 7851, Recife, PE 50732-970, Brasil, April 1995.
(Available from ftp.di.ufpe.br, pub/export/lallic/theses/deOliveira.ps.gz)

[deOldeQ94]
Anjolina Grisi de Oliveira and Ruy J. G. B de Queiroz.
Term rewriting systems with LDS.
In Proceedings of Brazilian Symposium on Artificial Intelligence, SBIA'94, 1994.

[deOldeQ95]
Anjolina Grisi de Oliveira and Ruy J. G. B. de Queiroz.
Proof transformation by rewriting (abstract).
In Abstracts of the 10th International Congress of Logic, Methodology and
Philosophy of Science, August 1995.  (To appear).

[deQGab92]
Ruy J. G. B. de Queiroz and Dov M. Gabbay.
An introduction to labelled natural deduction.
In 3rd Advanced Summer School in AI, Azores, September 1992.
(Available from theory.doc.ic.ac.uk,
theory/guests/deQueiroz/intro-lnd.{dvi,ps}.gz)

[Gab94]
Dov M. Gabbay.
Labelled Deductive Systems, Volume I - Foundations.
Oxford University Press (to appear). First Draft 1989. Current Draft, 465pp.,
May 1994.
Published as MPI-I-94-223, Max-Planck-Institut f\"ur Informatik, Im Stadtwald
D-63123 Saarbr\"ucken, Germany.

[GabdeQ92]
Dov M. Gabbay and Ruy J. G. B. de Queiroz.
Extending the Curry-Howard interpretation to linear, relevant and other
resource logics.
The Journal of Simbolic Logic 57(4):1319--1365, December 1992.

[Gir89]
J. Y. Girard, Y. Lafont, and P. Taylor.
Proofs and Types.
Cambridge University Press, 1989.

[How80]
W. A. Howard.
The formulae-as-types notion of construction.
In J.R. Seldin and J.R. Hindley (editors), To H. B. Curry: Essays on
Combinatory Logic Lambda Calculus and Formalism. Academic Press, 1980.

[KnuB70]
D.E. Knuth and P.B. Bendix.
Simple word problems in universal algebras.
In J. Leech (editor), Computational Problems in Abstract Algebra,
pages 263--297. Pergamon Press, 1970.


NOTES

(*) The $\eta$-reduction for the $\lor$ connective is framed as follows
[deQGab92]:


$\eta$-reduction-$\lor$

                   [x:A]                       [y:B]
              --------------($\lor$-intr)  --------------($\lor$-intr)
 c:A\or B     inl(x):A\lor B               inr(y):A\lor B
 --------------------------------------------------------($\lor$-elim)
  CASE(c,\upsilon{x}.inl(x),\upsilon{y}.inr(y)):A\lor B


                    \leadsto_\eta


                      c:A\or B


(`$\upsilon$' is an abstractor, similarly to `$\lambda$')

and the $\zeta$-reduction is defined as follows:

$\zeta$-reduction-$\lor$

               [x:A]          [y:B]
  c:A\or B     f(x):C         g(y):C
  -------------------------------------------($\lor$-elim)
  CASE(c,\upsilon{x}.f(x),\upsilon{y}.g(y)):C
 ----------------------------------------------(r)
 w(CASE(c,\upsilon{x}.f(x),\upsilon{y}.g(y))):W


                    \leadsto_\zeta


                    [x:A]           [y:B]
                    f(x):C          g(y):C
                 -----------(r)  -----------(r)
  c:A\or B        w(f(x)):W       w(g(y)):W
  -------------------------------------------------($\lor$-elim)
  CASE(c,\upsilon{x}.w(f(x)),\upsilon{y}.w(g(y))):W


Whilst `(r)' is usually restricted to an `elimination' rule, we have relaxed
this condition: it is only required that `(r)' does not discharge any
assumptions from the other (independent) branch, i.e. that the auxiliary
branches do not interfere with the main branch.

--
Anjolina Grisi de Oliveira and Ruy J.G.B. de Queiroz

Departamento de Informatica
Universidade Federal de Pernambuco (UFPE)
Caixa Postal 7851
Recife, PE 50732-970
Brazil
E-mail: {ago,ruy}@di.ufpe.br