|
From: Michael N. <Mic...@ni...> - 2004-03-29 04:41:02
|
[Part of this discussion seems to have fallen off hol-info; thanks to the Isabelle user who brought Rene's response to my attention.] Rene Vestergaard writes: > [...] More details can be found from my homepage > (http://www.jaist.ac.jp/~vester/) under the headings primitive > reasoning/proof theory, etc.. In particular, there are primitive > proofs of everything from confluence to standardisation and the > decidability of alpha-equivalence; the various presentations point > out the substantial problems that are glossed over in informal > approaches and that are likely to cause problems for Peter Homeier's > programme. Please do not hesitate to ask for further info. I have proved standardisation and the various obvious confluence results for a type isomorphic to the one Peter Homeier mentioned. I have a type 'a term with "constructors": VAR : string -> 'a term CON : 'a -> 'a term APP : 'a term -> 'a term -> 'a term LAM : string -> 'a term -> 'a term but where LAM x (VAR x) = LAM y (VAR y) I thus have the basic first order syntax quotiented up to alpha-equivalence. There is an accompanying structural induction principle that I used for the majority of the proofs I performed by induction on term structure. (Some, including the standardisation theorem itself, were done by induction on term size. This is how Barendregt proves it too.) My proof of standardisation and the finite-ness of developments followed Barendregt's chapter 11 as closely as possible. I found that the majority of the problems with this formalisation had little to do with the nature of my underlying type and more to do with other aspects of Barendregt's proof. For example, Barendregt's type \Lambda'* of terms with weighted variables is modelled as pairs of terms and maps from variable occurrences to non-zero natural numbers. (Section 11.2) Just specifying what happens to the map component of such a pair when a substitution occurs is a major pain. Indeed, Barendregt never really defines what a variable occurrence is. All of this is necessary for his proof of the well-foundedness of the \beta_0 relation. So, I agree that there are "substantial problems that are glossed over in informal approaches". But my experience suggests that these problems have relatively little to do with the fact that there is a quotiented type underneath. Michael. [There is a description of this work at http://web.rsise.anu.edu.au/~michaeln/pubs/merlin2003.pdf ] |