The Miser Project

Notes Folio n021000
The Well-Definedness Bind
Diary & Job Jar

miser>notes>
2002>10>

n021000a>
0.00 2014-04-17 19:32

Status Date Description
     
     
     
     
  2014-03-22 n021000: Simplify the synopsis explaining well-definedness in simple terms.  Express that it is essential in the mathematics and we want it to be honored when the mathematical structure is manifest in a computer implementation: The manifestation is a computational model, though.  The platonic illusion is sustainable, it would appear.
  2014-03-22 This raises the interesting problem concerning the existence of an individual, ob_fail, that signifies an explicitly-detected/-caused computation collapse.Suppose there is such an individual ,and suppose that ob.ap recognizes that individual such that ob.ap(ob_fail) applied to anything, including ob_fail, results in ob_fail.  Likewise, ob.ap(any,ob_fail) for computationally-determined any also results in ob_fail.  There are many problems with this.  In particular, the result of ob.d(x,y) must be ob.fail when x and y are computationally determined and at least one is ob_fail.  Secondly, operations like ob.e(ob_fail) must produce ob_fail, and ob.c(ob_fail,any) must be ob_fail, etc. 
   This needs to be reworked.  The key is that there can be no ob that corresponds to the fact of computationally-indeterminate.  Yet to have it be a simply individual the difference of which applies only for ob.ap seems peculiar.  While procedures might be devised to have exception values that are useful in the context for which those procedures are devised, building an exception case into ob.ap fails because outside of ob.ap the individual used can be used in all manner of situations without concern for ob.ap cases. 
   Perhaps the biggest objection to having such a special individual that can actually be manifest is the impact on partial-ordering of the Obs if such an individual is admitted.
  2014-03-22 There is nothing to prevent procedures being devised for which some agreed exception value is produced when certain computationally-determined conditions arise.   That is not intended in this case.  When something is not computationally-determined, there is no computationally-determined replacement for it. 
  2014-03-22 When ob.ap(f,x) is not computationally-determined, even though f and x are, there is no result.  Nothing is computationally-determined.   There is no computationally-determined result whatsoever in that case.  Some situations may themselves be determinable, but that is not generally so.  In an oMiser implementation, however collapse is recognized, the failed ob.ap evaluations do not provide any results for use in continuing computation.
  2014-03-22 I'm reluctant to assume any direct correspondence between partial functions and evaluations that are not computationally-determined.  We can say that when a function is not defined for an argument, x, that it is not computationally-determined for that argument.
  2014-03-22 Having something be computationally-determined goes with well-definedness on the computational side.  It means, of course, that the represented function is computable.  It is easy to state simple conditions on computationally-determined and not computationall-determined.  The hard part is that is necessary for p and x to be computationally determined for ob.ap(p,x) to be, but that is not sufficient for assurance that ob.ap(p,x) is indeed computationally-determined.  We have to know more about p to establish that.  We also have to be prepared for that being undecidable.  It is, after all, the halting problem.  
  2014-03-22 There is a difference between the well-definedness of some f:ob -> ob and some ob.ap(p): ob->ob.  There are also differences between partial functions and the procedures that correspond to them. 
  2014-03-21 n021000d: Create for development of the successor of n021000c (and there may be other companions as part of that).
  2006-06-08 N021000: The well-definedness bind.  This is important in the treatment of Peano Arithmetic too.  It is a Miser Note, because it relates to what I can do in oMiser with regard to preserving mathematics.  One thing I want to do here is decide what the proper name for ob.proc is.  In some sense it is ob.code, not ob.proc, and I need to think about that, because identity is all based on code even though the performance may be different.  But this is one of those cases where that doesn't matter.
done
2014-03-22
2014-03-21 n021000: Customize as a folio title page, version 0.01
done
2014-03-22
2014-03-21 n021000c: Create a revision history block that will lead to n021000d when it is different enough.
done
2014-03-22
2014-03-21 n021000c: Customize as a folio page, version 0.01
done 2014-03-21 Customize n021000a and n021000b for the new location, styles, and formatting
done 2014-03-21


The Construction and Content Material here was created in conformance with the style requirements of the
Site Repaving Project.  Check that folder for additional details of the approach to correction and upgrade.

 
0.00 2014-03-21-11:22 Initial Diary placeholder
 Create placeholder folder structure around this 2002-reserved topic

Construction Structure (Hard Hat Area)


visits to popular Miser Project pages

You are navigating the Miser Project.

created 2014-03-21-11:22 -0700 (pdt) by orcmid
$$Author: Orcmid $
$$Date: 14-04-17 19:32 $
$$Revision: 69 $