Procedures that determine the presence or absence of some condition can be viewed as (computational) propositions. In most programming systems, truth and falsity are represented implicitly in the operations of the system. Functions and expressions that yield those implicit representations are usefully taken as the intrinsic representations for predicates and propositions in the computational system.
In some systems, there are designated values that represent truth and falsity, and defined operations employ and produce those values in a consistent manner. Since there are only Obs in oMiser, if we are to fix particular values to signify truth and falsity, those values will be Obs.
However, the notion of truth in oMiser is more grounded in that it applies to what computational procedures in Miser do and do not determine. There is no fixed true/false distinction. Whether a result signifies the truth or falsity of something is a matter of the intention that is understood for the procedure that determines the result.
At the basic procedural level, there are merely the values that are produced based on some condition and there is not intrinsic notion of truth. One can consider this to be the case in all computational systems.
This separation of truth and falsity from just what computations produce is easily illustrated in the case of oMiser. In the formulation of oMiser there is only one given operation that determines any condition: function ob.d(x, y) on two given Obs x and y yields ob_a if x = y and ob_b if x ≠ y. Which of these two fixed Obs signifies truth of something depends on what the question happens to be: is truth to be the interpretation when x and y are the same or when they are different? Actual situations might depend on far more context than that much.
In order to express properties of ‹ob› in oMiser procedures, there does need to be an agreed convention for coding truth and falsity as Obs. The convention is to define ob_a to signify truth and ob_b for falsity in those situations where a truth-valued interpretation is called for. In this manner, predicates represented mathematically in ‹ob› can be manifest computationally in oMiser procedures in a direct manner.
Under this convention, the idiomatic is-singleton(x) defined as x = ob.b(x) can be manifest directly as ob.d(x, ob.b(x)).
The choice of ob_a and ob_b as results of ob.d(x, y) is not arbitrary. Although there is no inherent interpretation as truth values, there is the useful property that, by definition, ob.ap(ob_a, x) = ob.a(x) and ob.ap(ob_b, x) = ob.b(x).
The definition of ob.d(x,y) and the applicative interpretations of ob_a and ob_B are at the heart of application of oMiser to problems in logic, including representing logical conditions about oMiser itself.
This folio provides detailed considerations of how this is important with regard to ob.ap as a universal computational function and ‹ob› providing a model of computation, along with many useful definitions based on the interpretation of ob_a and ob_B as truth values.
n001100b: Computational Notions of Truth [latest]
n001100c: Initial Note
n010202: Homage to the Bit
n001000: Miser as Theoretical
Model
n001100a: Diary & Job Jar
|
created 2000-11-07-15:17 -0800 (pst) by
orcmid |