 |
status privacy contact |
|
|
Collaborative articulation of how abstraction and language is employed in the computational manifestation of numbers -- including analysis of the role of syntax, semantics, and meaning in the specification and use of software interfaces.
Recent Items Archives |
2008-05-06Miser: The Logic of Ot
Technorati Tags: orcmid, Miser, computation models, theoretical structures, FOL=, first-order logic, equational identities, first-order theory In the narrow sense, logic is the theory of valid arguments Miser demonstrates a model of computation. The specification of Miser establishes the functional requirements for a computing machine (the mechanism). The machines are typically implemented by software programs operated on conventional digital computers. That this can be done at all is a demonstration of how well digital computers are useful for manifestation of abstractions. While it is appropriate to think of a Miser as a machine with a variety of physical realizations, there is a mathematical theory that dictates the essential characteristics that each realization is expected to manifest. This is by design. We want Miser to be amenable to mathematical reasoning and analysis. The mathematical theory determines the correct behavior of Miser implementations. Even so, no result in the mathematical theory can ever be a proof about a Miser implementation. We want to develop an appreciation for how this is so and how there remains an useful connection between theories and concrete realizations even though the connection is a bridge that the theory can never cross. The mathematical theory is essentially pure logic applied to a simple subject matter: the Miser Obs and functions over them. It is also the case that Miser procedures perform in logic-resembling ways and can achieve what is known as a computational logic. Both of these conditions require that we be careful about our demands on logic and how they will be expressed. We need to look at how the theory for Miser is expressed as a logical theory as well as how logic is expressed in Miser procedures (that is, by computational means). This reliance on a logical theory will assist our differentiation among computation, logic, and mathematics. This will, in turn, help us clarify the relationship between procedures and functions and algorithms for functions as we look more closely at the Miser computational model. The logical theory for oMiser, the foundation system, is symbolized Ot, short for Ob theory. It is an application of First-Order Logic. 1. First-Order LogicThe logical theory for Miser is mostly expressed in an informal style. Most of the assertions under the theory are in the form of equations or identities: equalities and inequalities. Although there is not much need for a full-up expression in a formal logic, there is always an equivalent formal expression using First-Order Logic with equality (FOL=). The FOL= logical symbolism employs the following forms:
A common order of precedence of the operations is indicated in the progression. The components of the equality and inequalities can be constants, variables, and expressions involving functions of operands that are the same kind of components. These are not applicative expressions and should not be read as Frugalese applicative operations (just yet, if ever). A basic introduction to FOL notation is available on-line in the MIT Open Courseware [2]. There are other on-line descriptions [4, 6]. These should provide enough background to be able to read the formalisms of Ot. The specific form used here is that described in the Handbook of Mathematical Logic [1]. Leisurely expositions with many examples and exercises are available in the books by Lemmon [3] and Suppes [5]. 2. Informal ExpressionThe informal expression allows us to avoid heavy use of special symbols. For example, an axiom of equality,
could be expressed informally for Ot as
There are further examples to be found among the posts on Numbering Peano and in other Miser Project materials. 3. Ot as a Logical TheoryFor Ot, there are additional constants to be introduced (e.g., ob_A, ob_B). We also presume a variety of functions (e.g., ob.a, ob.b, ob.ap). These and other additions to FOL= constitute Ot. In particular, we assume that the variables of quantifiers (x and y in ∀x, ∃y) refer to Obs. Because the domain of discourse, as it is known, is the Obs and only the Obs, how functions are represented in Ot becomes an interesting topic. The same is true for additional predicates (i.e., beyond the predicate implicitly associated with "="). We will explore these matters in further posts and articles of the Miser Project. For now it is useful to point out that there is no direct way to express something about all/any functions or all/any predicates using FOL= (a consequence of being first-order). When we speak in such a way, it will have to be informally and outside of Ot. That situation is also to be explored further.
Comments: Post a Comment |
|
|
You are navigating the Miser Project |
template created 2004-05-31-22:34 -0700 (pdt)
by orcmid |