Difficult questions. Regarding any term with an undefined subterm as undefined is simplest - then you can have theorems like (A DIV B) TIMES B = A without side conditions.
Problem is, though, you want to be able to write "if A NOT EQ [] THEN HD A ..." which can have an undefined subterm (HD A). I found the case for the "Logic of Partial Functions" strong - I describe it, and give references to it, in my TPHOLS 98 Track B (or whatever it was called then) paper, which is at http://users.cecs.anu.edu.au/~jeremy/pubs/rewr/wip-submitted/tphols.dvi Cheers, Jeremy Michael Norrish wrote: > On 10/04/13 05:46, Cris Perdue wrote: > > >> I think this systematizes the approach that leads to using x != 0 ==> recip >> x * >> x = 1 as a specification for reciprocal, or Konrad's example with DIV and >> MOD. >> Hopefully I am not missing something here. >> > > Taking definedness to the level Freek is discussing would, I think, not let > you > prove that > > x DIV 0 = x DIV 0 > > at least if you were in the "meta-world" where you were paying attention to > the > D(..) predicate. > > It's problems like this that set off alarms with many. > > More examples: > - should (x DIV 0) * 0 = 0 be a theorem? > - should (x DIV 0) + 1 > x DIV 0 be a theorem? > > Michael > > > ------------------------------------------------------------------------ > > ------------------------------------------------------------------------------ > Precog is a next-generation analytics platform capable of advanced > analytics on semi-structured data. The platform includes APIs for building > apps and a phenomenal toolset for data science. Developers can use > our toolset for easy data analysis & visualization. Get a free account! > http://www2.precog.com/precogplatform/slashdotnewsletter > ------------------------------------------------------------------------ > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
