On Mon, September 29, 2008 12:09 am, Chris Rowley wrote: > Professor James Davenport wrote -- >> > Thus I would allow multiple definitions but insist that they are >> > compatible. >> A plausible point of view. It makes the concept of non-cyclicity >> non-deterministic, since it might depend which definitions one used: I >> would wish to insist on NEVER CYCLIC. > > Agreed. With 'proof'? With as much of a 'proof' as can be provided, i.e. the proofs are dependent on the actual definitions (as opposed to merely the semantics) of all the objects involved. > >> > Moving on, one could usefully insist on a _mathematical_ proof of all >> > of such things: compatibility, non-cyclicity, finiteness etc. Or not! >> Non-cyclicity is a feature of the entire graph of CDs, and therefore >> subject to change, whereas consistency of definitions in a CD is a fact >> of >> that CD (assuming that the SEMANTICS, as opposed to the way they are >> expressed, of objects depended on does not change, and this is illegal). > > Not sure that I agree here. Non-cyclicity for one CD is surely only a > property of the 'dependency subgraph generated by the contents of that > CD', not the entire dependency graph of CDs. And the former is > exactly the subgraph whose nodes need to be studied (in greater > detail) when checking consistency. Not quite, would be my view. If I am (a theorem-prover) interested in checking consistency, then I can stop when I reach a node I 'understand' [of course, if I 'understand' it incorrectly, all bets are off, but that's OM for you], whereas another theorem-prover might have to descend.
So, if I have two different definitions (DeFMPs) of aardvarks in terms of wombats, and my theorem prover understands wombats, then these two definitions are all that the ThP needs to look at. If in addition, we have a definition (DefMP) of aardvarks in terms of mobats, and FMPs defining moBats in terms of wombats, our ThP is happy. If I have a ThP that understands mobats but not wombats, it does not know that these are consistent. I can make it happy by adding (the right) definitions of wombats in terms of mobats. both ThP are happy, but with different traversals of the graph. BUT, if I make the wonbat=>mobat and mobat=>wombat into DefMP, both ThP are still happy (since a DefMP is no more than a FMP as far as a strict ThP is concerned), but I have now introduced circularity, and a ThP that understand neither wombats nor mobats would go in a loop. James Davenport Hebron & Medlock Professor of Information Technology Formerly RAE Coordinator and Undergraduate Director of Studies, CS Dept Lecturer on CM30070, 30078, 50209, 50123, 50199 Chairman, Powerful Computing WP, University of Bath OpenMath Content Dictionary Editor IMU Committee on Electronic Information and Communication _______________________________________________ Om3 mailing list [email protected] http://openmath.org/mailman/listinfo/om3
