Dear Andreas,

I'm juping in the middle of the discussion (not following the
context)...

Andreas Rossberg <rossberg@ps.uni-sb.de> wrote:

> If you add lambdas (under recursion) things get MUCH harder. Last time I
> looked the problem of equivalence of such types under the equi-recursive
> interpretation you seem to imply (i.e. recursion is `transparent') was
> believed to be undecidable.

It IS a difficult problem, but there is actually a hope.  Solomon
proved in '78 that the equivalence problem between a limited form of
parametric types reduces to the equivalence between deterministic
pushdown automata.  The latter had been a long-standing big problem.
Very recently ('97), it was solved: decidable.  If you are interested,
look into these papers.

@InProceedings{Solomon78,
  author =       "Marvin Solomon",
  title =        "Type Definitions with Parameters",
  booktitle =    "Conference Record of the Fifth Annual {ACM} Symposium
                 on Principles of Programming Languages",
  address =      "Tucson, Arizona",
  organization = "ACM SIGACT-SIGPLAN",
  month =        jan # " 23--25,",
  year =         "1978",
  pages =        "31--38",
  note =         "Extended abstract",
}

@InProceedings{Senizergues97,
  author = 	 "G{\'{e}}raud S{\'{e}}nizergues",
  title = 	 "Decidability of the equivalence problem for
		  deterministic pushdown automata", 
  OPTcrossref =  "",
  OPTkey = 	 "",
  OPTeditor = 	 "",
  OPTvolume = 	 "",
  OPTnumber = 	 "",
  OPTseries = 	 "",
  OPTpages = 	 "",
  booktitle =	 "Proceedings of INFINITY'97",
  year =	 "1997",
  OPTorganization = "",
  OPTpublisher = "",
  OPTaddress = 	 "",
  OPTmonth = 	 "",
  OPTnote = 	 "",
  OPTannote = 	 ""
}

Hope helps,

Haruo
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners