THE DECISION OF EQUALITY IN RECURSIVE TYPES, AN EARLY PROOF
Concerning the Syntax of ALGOL 68 by Claude Pair
Algol Bulletin n. 31, March 1970
Here is a paper by Claude Pair which is to my knowledge the first which
addresses the decision of the equality in recursive types. The framework
is this of ALGOL 68 and has a slightly different terminology from the one
of 2002.
-
ALGOL68 today
-
mode
type
-
struct
record
The problem is clearly presented on Page 17, the proof is done in language
theory with no clear distinction between the concrete and the abstract
syntax. It relies on the existence of a unique fixpoint. The existence
of the decision procedure is alluded on the last lines of page 25 "It may
be remarked that the test for equality of the components of the solution
of a system, given by proposition 4, lends itself well to being programmed"
but the proof provides clearly a decision algorithm.
The document
The document is here.
Who is Claude Pair ?
Claude Pair was a prominent figure of computer science research in France
and more specifically in Nancy. He graduated from Ecole Normale Superieure
of Paris. He was the founder of the Centre de Recherche en Informatique
de Nancy (now Loria), president of the computer science section of CNRS,
president of the University known as Institut National Polytechnique de
Lorraine, director des Lycees at the French Ministry of National Education,
rector of the academy of Lille. He received the Montpetit Price from the
French Academy of Science and the grade of commandor of Legion d'Honneur
(see the picture below when he received the decoration from Hubert Curien).
He was also my thesis supervisor. He is now retired and his current main interest is education
for disadvantaged children.
-
Pierre LESCANNE
-
Ecole Normale Superieure
-
F69364 LYON Cedex 07 FRANCE
-
Pierre.Lescanne@ens-lyon.fr
Last modified: Tue Sep 23 18:19:11 CEST 2008