Predicate
Logic with Definitions and the General Concept of Algorithm
Victor Makarov
Introduction
Development of more general (and
more suitable for applications) precise concepts of algorithm is important both
for mathematics and computer science [1, 2, 3]. In [4] the following concept of
abstract algorithm was suggested:
Any algorithm is defined in a
certain mathematical theory (for example, graph algorithms in the graph
theory). That is, the concept of algorithm is inseparable from the concept of
mathematical theory and actually is subordinate to it because before the
development of an algorithm we should have a mathematical theory. An algorithm
is a definition (of some special kind) in this theory.
The aim of this paper is to suggest a new (more precise and simple
comparing to the author’s previous papers [4, 5]) practical formalism –
Predicate Logic with Definitions (or D-logic or simply DL) – for defining
mathematical theories and writing definitions inside the theories. DL is a modification
of the first-order logic by adding to its main syntactic constructs – terms and
formulas – a new syntactic construct, called definition. As an example, we show
that the abstract state machines of Gurevich[2] can be naturally represented in DL.
1. Mathematical theories
To make the concept of abstract algorithm precise, we at first should
have a precise definition of the concept “mathematical theory”. Fortunately,
the last century’s work on the foundations of mathematics has provided such a
definition [6, p. 215], accepted by the most of mathematicians:
A mathematical theory T is an
extension of the first-order theory ZFC (Zermelo-Fraenkel
set theory with the axiom of choice) by adding to ZFC a finite number of new
constants c1, … , ck (k ³1)
and an axiom A, implicitly defining these constants.
In DL,
the theory T can be defined in the following way:
T := def[c1,…,ck;
A];
The name of the theory T must be
an unique identifier, the constant names c1,…,ck
are identifiers or operators (an operator is a finite sequence of such symbols
as +, -,
*,/,
… ). The expression “def [c1,…,ck;
A]” (and any expression of this form) is called a definition of constants. The formula A is called the formula of
this definition. A similar expression of the form “(x1, …, xm; P)”, where x1,
…, xm (m ³1) are new variable names
and P is a formula is called a definition
of variables. A primitive definition
is a definition of constants or a definition of variables. The expression “T := def[c1, …, ck; A]” is called a theory definition.
Let z be any tuple (z1, …, zk) where z1,
…, zk are some terms, and the formula A¢ is
the result of substitution in the formula A the terms z1, …, zk instead of the constants c1, …, ck,
respectively. The tuple z is called a model of the theory T if the formula A¢ is a
theorem (note that this definition differs from the definition of model in the
model theory).
The formula A¢
can be written in DL as Subst(A, T, z) where Subst is a standard
symbol of DL and appropriate axioms for substitution are provided in D-logic.
The statement “z is a model of the theory T” (which can be expressed by the formula A¢) can also be written is DL as “z Î T”. The statement “the theory T is consistent” can be written as “E[T]”. Note that the formula “z Î T ® E[T]” is a theorem of D-logic. The formula E[T] can be translated into the classical first-order logic as $y1 …$ykA1 where y1, …, yk are new variable names and A1 = Subst(A, T, (y1, …,yk) ).
2. Types and typed
definitions
A type is a term or a primitive definition. A typed definition of constants has the following form:
def[c1:t1, … ,ck:tk; A] (k ³ 1)
where c1, …ck are new constant names, t1, …, tk are some types.
This typed definition can be translated into the following equivalent untyped one:
def[c1,…,ck ; c1 Î t1 & … & ckÎt k & A];
Mostly typed definitions are used in DL, because it allows to assign nontrivial types to most of terms and that can be useful. The trivial type is the type “set” which can be defined by the following definition:
set := def[anyset; true];
Typed definitions of variables can be defined in the similar way.
3. Internal
definitions
Having a mathematical theory T, we need a notation for writing definitions
inside the theory T. In DL, there are three kinds of such definitions: abbreviations, explicit definitions and implicit definitions.
An abbreviation has the following form:
T ::
N :=
Q
Here Q is a term or a formula, N is an unique in T identifier – the name of Q. This abbreviation means “In the theory T, the name N can be used instead of Q.” The name N can not occur in Q, directly or indirectly.
An explicit definition has the following form:
T :: N := def[c1,…,ck; A]; (k ³ 1)
and introduces into the theory T new constants c1, …ck with the new axiom A which is usually an equality or a conjunction of (possibly conditional) equalities. The name N can be omitted.
An implicit definition has the following form:
T :: T1 := sdef[c1, …,ck; A] (k ³ 0)
(no
restrictions on the formula A)and introduces a new theory T1 which is the
extension of the theory T by adding to the theory T the constants c1,
…, ck and the axiom A. The
expression “sdef[c1,…,ck; A]” is a form of the
primitive definition of constants. Implicit definitions can be used for
algorithm specification. Usually, the formula E[T1]
must be a theorem of the theory T.
4. The language of D – logic
Arity in DL is any finite sequence of the letters F, T, D (from Formula,
Term, Definition). For each logical (and other primary)
symbols we assign arity as follows:
true : F;
false : F;
~ (negation) FF;
&, Ú, ®, ≡ (binary logical symbols) FFF;
H (Hilbert’s epsilon-symbol) DT;
Frm (formula of definition) DF;
E, A (quantifiers) DF;
E, A (restricted quantifiers) DFF;
Î (is a model of)
TDF;
Subst (substitution for terms) TDTT;
Subst (substitution for formulas) FDTF;
Subst (substitution for definitions) DDTT;
= (equality) TTF;
Î (is a member of)
TTF;
® (A®B is the set of all functions from A to B)
TTT;
For other standard
set-theoretic symbols their arities are assigned in an
obvious way. Then the sets of terms and formulas can be also defined in an
obvious way. Let us note that the terms of the form Subst(y,
d, z) can also be written as d(z).y, or simply z.y, if
we can determine from the context the definition d (for example, analyzing the
type of the term z). The same applies
also to formulas and definitions of the form Subst(q, d, z).
5. Axioms of D-logic
Below d is a definitional
variable, z is a free variable. Definitional
variables are used for representing axiom schemes. The “formulas” with
definitional variables still will be called formulas but one should remember
that such a “formula” actually represents an infinite set of formulas. The
following formulas are axioms:
1)
Any
tautology;
2)
z Î d ® H[d] Î d;
(epsilon-axiom)
3)
E[d]
≡ H[d] Î d (defining axiom for E)
4)
Defining
axioms for other logical symbols;
5)
Axioms
for equality;
6)
Substitution
axioms;
7)
Nonlogical axioms
(ZFC).
6. Inference rules
1) From p and p®q infer q;
2) From p and z Î d infer Subst(p, d, z);
3) From p ® (z Î d) infer p ® A[d], if p does not contain free occurrences
of z;
4) From (z Î d) ® p infer E[d] ® p, if p does not contain free occurrences of z;
Other derived inference rules
can be added.
7. D-calculus
D-calculus is D-logic without nonlogical axioms.
Theorem. D-calculus is consistent, that is the formula “false” can not be
derived in D-calculus.
8 . Abstract
state machines (ASM)
An abstract state machine A[2] is a triple <S, I, Step> where:
S – a set (of states),
I Í S – a set of initial states,
Step: S ® S, a one-step transformation of S.
There are some important additional conditions:
1) Every state is a first-order structure of the same finite vocabulary V;
2) The one-step transformation Step does not change the base set of any state.
Let the vocabulary V be a nonempty set {c1,…, ck, f1, … , fm} where c1,…,ck (k ³ 0) are constant names (that is, 0-ary function names) and f1, … , fm (m ³ 0) are function names of the arities a1, … , am respectively and a I > 0 for each i = 1, … , m.
Then the function Step can be defined in D-logic as follows:
G := def[U:set, c1:U, … , ck:U, f1:U^a1®U, … , fm:U^am®U];
G :: def[Step:G; Step.U = U & <other defining axioms for Step> ];
Here U^ai
denotes the set U if ai =1, otherwise it
denotes the direct product U´ … ´U (U occurs ai
times in this direct product).
[1] A.N. Kolmogorov and V.A. Uspenski. On the definition of algorithm. Uspekhi Mat. Nauk, 13 (1958), 3-28 (Russian).
[2] Yuri Gurevich.
Sequential
http://research.microsoft.com/~gurevich/Opera/141.pdf
[3] Yannis N. Moschovakis. What Is an Algorithm? Mathematics Unlimited – 2001 and beyond, ed. by B. Engquist and W. Schmid, Springer, 2001, pp. 919-936. Also see: http://www.math.ucla.edu/~ynm/papers.htm.
[4] Victor Makarov. Towards a theory of abstract algorithms. Nauchno-Technicheskaya Informatsiya, ser. 2, 1982, N9, pp. 35-40 (Russian). Also see: http://home.nyu.edu/~yvm204/vm/vm.htm
[5] Victor Makarov. MSL – A
Mathematical Specification Language, in:
“Logical Foundations of Computer Science – Tver’92”, Lecture Notes in
Computer Science, Vol. 620 (1992), pp. 305-313.
[6] Dieudonne
J.A. A Panorama of Pure Mathematics.