Programs 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.
For Miser, we have the opportunity to choose among some interesting representations for truth and falsity. This note explores that opportunity and constructs a rationale for the particular choice of truth values and its power in idiomatic expression of programs and propositions using Miser.
Content
In any programming system that is adequate for expressing practical, general-purpose computation, there are an arbitrary number of ways to represent the notions of truth and falsity as well as the standard propositional forms of logic: A and B, A or B, not A, etc. Representing truth and falsity is not much different than representing any externally-based "fact" or even representing arithmetic It is simply a potential intention in the design of the program -- something being modeled.
At this point, there is nothing that says we must represent truth with a program or that a given program does model truth (of something). Let us concede that computer programs can be constructed to model truth (of something). If the programming system is complete in its ability to represent all computable functions, then we can take as given that there is a rich variety of ways that truth (of anything) may be modeled.
We want to narrow the investigation to intrinsic representations of truth which are seen to be designed into programming systems and that are essential to their general-purpose function. By intrinsic is meant that values of the intrinsic "truth" representation arise automatically as part of the defined operations of the programming system. The "truth" representations derive immediately from design principles reflected in the computational mechanism.
In the C Programming Language [Harbison95], it is clear that there are intrinsic representations for truth and falsity using the
intvalue1for truth and0for falsity. These values are produced by the relational and logical operations:==,!=,>,<,!,&&,||, etc. It is consistent with this representation that conditional operations, especially theifoperation (and also&&,||, and unary!), interpret0as falsity and any otherintvalue (including1) as truth.This use of arithmetic values
0and1(or0and everything but0) is a commonplace idiom for intrinsic truth values in programming systems. There are a number of appealing qualities, including availability of simple machine-language instructions for enacting programming-language operations expressed in these terms. There is a certain legitimacy as well: George Boole used an arithmetic restricted to 0 and 1 in the original development of symbolic logic [Boole1854].In some programming languages, such as Pascal and members of the Algol family, there is a separate
Booleandata type which is restricted to the valuestrueandfalse. Values of this type are delivered by the relational operations, and they are required by logical operations and conditional operations, especially theifandwhileoperations.Relying on Boolean data types can make it easier to tell where truth representations likely are used in a program. Sun's Java language and Microsoft's C# language use separate Boolean data types (named
booleanandboolrespectively) for their intrinsic truth representations.
In the earliest "functional language," LISP, the fundamental data type is a form of list structure. The simplest list structure is
NIL, the empty list.[More here on how that worked, and also the use of
#trueand#falsenow too.]
We are looking at those aspects of a computational mechanism by which conditional behavior is achieved: the means by which different actions are taken depending on whether a specified condition is satisfied or not. This has us be interested in two things:
Condition Determination: Those operations that determine whether some condition is satisfied or not. These operations correspond to primitive propositions.
Conditional Operation: Those operations that vary behavior of the program based on the result of a determined condition. These operations can be identified with composition of more complex propositions and functions from the primitive propositions.
In the examples of C Language and Lisp-based languages, we see that there are specific counterparts of these ideas.
In the Miser system, there is only one primitive for condition determination: the ob-match function. This function determines whether one operand is the same Miser Ob as the other operand. The result of ob-match(x, y) is one specific Ob, ob-YES, when x equals y. Ob-match(x, y) is a different but specific Ob, ob-NO, when x does not equal y.
It is the case that
ob-match(x, x)
yields the intrinsic representation of Miser "truth" for any determined x. Likewise,
ob-match(x, ob-quote(x))
yields the intrinsic representation of Miser "falsity," since ob-quote(x) is guaranteed to be different than x for x any determined Miser Ob.
The choice of ob-YES and ob-NO is what interests us. We have the following requirements:
- R1. ob-YES and ob-NO are uniquelly-distinguished Obs.
R2. ob-apply(ob-YES, x) and ob-apply(ob-NO, x) are usefully-different functions and can serve as idioms for conditionally-determined operations.
R3. The definitions of Miser "truth"-values is based on differentiation of Obs and not differentiation of the applicative interpretations of Obs.
An essential quality for intrinsic truth is that the result of condition determination "get us somewhere." That is, something can be done with an intrinsic-truth value that moves a computation toward a determined result.
In Miser, there is no distinct conditional operation. Basically, the only operation that moves computations forward is ob-apply. Conditional behavior is by giving applicative interpretations to ob-YES and ob-NO that lead to well-defined and useful differences in behavior.
The conditional behavior that we use is to choose between two alternatives. It is done this way:
ob-apply(ob-YES, x) = ob-a(x)
ob-apply(ob-NO, x) = ob-b(x)
for x any determined Ob.
As a consequence,
ob-apply(ob-YES, ob-c(x, y)) = x
ob-apply(ob-NO, ob-c(x, y)) = y
for x and y any determined Obs.
And this is sufficient to obtain any desired conditional behavior, since we can use
ob-apply(ob-apply(ob-YES, ob-c(x, y)), z) = ob-apply(x, z)
ob-apply(ob-apply(ob-NO, ob-c(x, y)), z) = ob-apply(y, z)
as an idiom for arbitrary conditional behavior, corresponding to
if p then x(z) else y(z)
Assuming that Miser is computationally complete, then whatever computational propositions there are, we expect that we are able to represent all of them with this much conditional-behavior machinery.
Why we didn't use an applicative definition for truth and employed ob-YES and ob-NO as definite Obs.
The initial simplistic assumption that lets us talk about propositions pretty much at all. (This isn't actually necessary in general, but it seems necessary for computational propositions.)
The basic propositional forms and some demonstrated propositional functions.
Distinguishing between operating with truth functions and predicates and creating propositional forms. Maybe just a little.
See if there is anything in the computational logic sphere that we can borrow and illustrate here.
The dual of truth applies in programming systems.
The preference of Yes/No to True/False in reflecting computational truth (condition determination)
Inferring propositions versus the use of fixed forms for propositions. What it means for computational inference procedures.
Looking at the insight that the propositional calculus is about the sense of statements, not the literal surface syntax of statements, but that a formal view is indispensible for getting some certainty on being able to discern the proposition in a statement.
Dealing with propositions that are time-sensitive -- that is, there are predicates the determination of which depends on the state of the system at the time the predicate is asserted.
Dealing with the opacity and ambiguity of Obs as propositions, and discerning the form of the proposition from an applicative expression on Obs.
Issues of decidability in the ability to perform computational logic using Obs as computational propositions. Issues of computability with regard to propositional algebra.
Tying the two together. We can start with distinguished forms for and, or, not, implies, cond, and so on. That will certainly let us apply logical analysis and determine tautologies, etc.
Dealing with the prospect of undefined elements. We may have to do something about that. What happens when an operand-form does not yield a determined Ob, and other stories.
- [Boole1854]
- Boole, George. An Investigation of the Laws of Thought on which Are Founded the Mathematical Theories of Logic and Probabilities. Macmillan (Toronto, London: 1854). Dover edition (New York: 1958) with all corrections made in the text. ISBN 0-486-60028-9.
- [Burge75]
- Burge, William H. Recursive Programming Techniques. Addison-Wesley (Reading, MA: 1975). ISBN 0-201-14450-6.
- [Harbison95]
- Harbison, Samuel P., Steele, Guy L.,Jr. C, A Reference Manual. ed.4. Prentice-Hall (Englewood Cliffs, NJ: 1995). ISBN 0-13-326224-3 pbk.
To be included:
Boyer and Moore, Computational Logic as an example of interpretation of computational forms as propositions and predicates.
Use the ANSI standard for C rather than Harbison and Steele.
Reynolds for the use of closed lambda-calculus forms for truth and falsity.
Abelson and Sussman for how it is done in lisp-like systems, namely Scheme.
Anything about propositions versus the truth-value model that is useful here.
- Version 0.20: Introduce ob-YES and ob-NO (orcmid)
- In looking at other problems around indeterminate results, I settled on YES and NO as better general responses than TRUE and FALSE. This provides a tie-in to having determined results. This edition provides initial capture of these ideas.
- Version 0.10: Initial Draft (orcmid)
- Sketch the basic question and why I am interested in it. Explore how this is typically done.
created 2000-11-07-15:17 -0800 (pst) by orcmid
$$Author: Orcmid $
$$Date: 04-01-06 13:03 $
$$Revision: 8 $