Recursion
Russell Storms
Can recursion (not reduced to iteration) be implemented in first-order
logic?
--
---------------------------------------------------------------------------
Russell L. Storms
Department of Computer Science Work: 408.656.2174
Naval Postgraduate School, Code CS/Zk Fax: 408.656.2814
833 Dyer Road Monterey, CA 93943-5118 USA Email:
sto...@cs.nps.navy.mil
Internet: http://www.cs.nps.navy.mil/people/phd/storms/
Ian Sutherland
In article <320764...@cs.nps.navy.mil>,
Russell Storms <sto...@cs.nps.navy.mil> wrote:
>Can recursion (not reduced to iteration) be implemented in first-order
>logic?
I think you'll have to say a bit more about what you mean, e.g.:
- what do you mean by "implementing" something in
first-order logic? First-order logic is a declarative
language, not an imperative language.
- when you say "first-order logic", do you mean with no
nonlogical axioms, or are we allowed some arithmetic?
- what do you mean by "recursion" and "iteration" in a
first-order language? Do you mean recursion and
iteration in some computational process _described_ in
first-order logic, or do you mean statements that somehow
refer to themselves (in which case I really don't see
what "iteration" means)?
--
Ian Sutherland
i...@eecs.nwu.edu
Sans Peur
Dr. Richard Botting
Oddly I've been thinking about a related area recently.
The background is using lower predicate calculus to express
requirements - in particular assumptions that software will
be making about it's environment. Now it is very handy to be
able to define new predicates in terms of given predicates:
sibling(x,y) ::= not(x=y) and for some z(parent(z,x) and parent(z,y)).
You can justify this because 'sibling' can always be removed
form any wff and replaced by the full expression.
But what justifications are there for writing:
ancestor(x,y) ::= parent(x,y) or for some z(parent(x,z) and ancestor(z,y)).
Whitehead and Russel are able to define ancesral relations by a second
order quantification...
As far as I can tell attempts to use a Dana Scott style domain based
on the Booleans plus 'undefined'=\bot gives the wrong answer.
But, there is an argument based on setting up a partial order
on predicates:
F square_less_than_or_eq G iff
for all x( F(x) implies G(x) ).
and showing the this is a CPO, and the above definition generates
an ascending sequence of predicates.
Has this been published anywhere before?
--
dick botting http://www.csci.csusb.edu/dick/signature.html
Disclaimer: CSUSB may or may not agree with this message.
Copyright(1996): Copy freely but say where it came from.
Ilias Kastanas
In article <320764...@cs.nps.navy.mil>,
Russell Storms <sto...@cs.nps.navy.mil> wrote:
>Can recursion (not reduced to iteration) be implemented in first-order
>logic?
Without restrictions, trivially yes. Set theory (ZFC say) is in
1st-order logic, and it contains all of mathematics.
Recursion on the integers needs much less: definitions and proofs
of theorems can be done in PA (Peano Arithmetic), and in even weaker
system. More complicated kinds or domains need more.
Maybe you have in mind statements like "transitive closure is not
1st-order". It is implied that this holds over the collection of all
finite models (e.g. finite graphs); it is a very weak form of 1st-order
logic.
Also, "implemented" can mean various things. There is no "algorithm
to do logic"; it's an undecidable problem. Limited to propositional
logic the problem is decidable but almost surely intractable (if P != NP).
Existing forms of programming that deal with logic, in various ways,
handle only fragments for which reasonably fast algorithms exist.
Ilias
Steffo Weber
|> Can recursion (not reduced to iteration) be implemented in first-order
|> logic?
If you want to know which type of theories or better
complexity classes can be captured by FOL, then you
should have a look at Ehrenfeucht-Fraissee Games.
Graph Accessibility, for example cannot be expressed
in FOL (without function symbols).
You can, however, add new operators e.g. TC
(transitive closure) to improve expressibility.
As for some literature, take a look at
Finite Model Theory.
Steffo
ilias kastanas 08-14-90
In article <4uaajd$o...@news.csus.edu>,
Dr. Richard Botting <di...@silicon.csci.csusb.edu> wrote:
@Oddly I've been thinking about a related area recently.
@The background is using lower predicate calculus to express
@requirements - in particular assumptions that software will
@be making about it's environment. Now it is very handy to be
@able to define new predicates in terms of given predicates:
@ sibling(x,y) ::= not(x=y) and for some z(parent(z,x) and parent(z,y)).
@You can justify this because 'sibling' can always be removed
@form any wff and replaced by the full expression.
@
@But what justifications are there for writing:
@ ancestor(x,y) ::= parent(x,y) or for some z(parent(x,z) and ancestor(z,y)).
@
@Whitehead and Russel are able to define ancesral relations by a second
@order quantification...
@
@As far as I can tell attempts to use a Dana Scott style domain based
@on the Booleans plus 'undefined'=\bot gives the wrong answer.
@
@But, there is an argument based on setting up a partial order
@on predicates:
@ F square_less_than_or_eq G iff
@ for all x( F(x) implies G(x) ).
@and showing the this is a CPO, and the above definition generates
@an ascending sequence of predicates.
@
@Has this been published anywhere before?
The partial order on predicates might not be very helpful. If you
have a chain F1(x), F2(x) ... an upper bound would in general be something
like F1(x) & F2(x) & ..., an infinitary formula not expressible in the
Predicate Calculus.
Regarding the domain problem: for predicates interpreted in a cpo
(or program) Boolean + undefined seems necessary; for predicates _about_
a cpo Boolean is enough.
What you are doing with 'ancestor' does not involve full second-
order logic; it is an instance of Inductive Definability. The usual set-
ting is a formula F(S) with a relation symbol S that occurs positively
('not negated', directly or indirectly ( S => ...) ). Then F is monotonic
in S and can be iterated to produce fixed-points. As an example, on the
structure of arithmetic, where formulas define arithmetical (Sigma-0-n)
sets, I.D. produces Pi-1-1 sets. Full 2nd-order would be Pi-1-n.
Still, it does exceed 1st-order... Pi-1-1 is much more complicated
than arithmetical. There is theory on I.D. and you might be able to
use it, but you will have moved beyond the Predicate Calculus.
Ilias
Ulrike Sattler
Russell Storms wrote:
>
> Can recursion (not reduced to iteration) be implemented in first-order
> logic?
>
You might want to have a look on Description Logics with transitive
closure on roles or cyclic definitions. Most of these Description Logics
are decidable fragments of first order logic, but in the presence of
cyclic definitions or the transitive closure of roles, they are
stronger. For example, some of these extensions allows us to define
recursive structures such as trees or lists, see for example
@InProceedings{GiLe94b,
author = {Giuseppe {De Giacomo} and Maurizio Lenzerini},
title = {Boosting the correspondence between description
logics and propositional dynamic logics
(extended abstract)},
booktitle = AAAI-94,
year = {1994},
}
@TechReport{Baad90,
author = {Franz Baader},
title = {Terminological Cycles in {KL-ONE}-based Knowledge
Representation Languages},
institution = DFKI,
address = {Kaiserslautern, } # Germany,
number = {RR-90-01},
year = {1990},
note = {An abridged version appeared in {\sl Proc.\ of the 8th
Nat.\ Conf.\ on Artificial Intelligence AAAI-90}, pp.
621--626},
}
@TechReport{Baad90b,
author = {Franz Baader},
title = {Augmenting Concept Languages by Transitive Closure of
Roles: An Alternative to Terminological Cycles},
institution = DFKI,
address = {Kaiserslautern, } # Germany,
number = {RR-90-13},
year = {1990},
note = {An abridged version appeared in {\sl Proc.\ of the
12th Int.\ Joint Conf.\ on Artificial Intelligence
IJCAI-91}, pp. 446--451},
}
@InProceedings{Schi94,
author = {Schild, K.},
title = {Terminological Cycles and the Propositional
$\mu$-Calculus},
booktitle = KR-94,
pages = {509--520},
address = {Bonn},
editor = {J. Doyle and E. Sandewall and P. Torasso},
publisher = MK,
year = {1994}
}
and have decidable satisfiability problems!
Hope this helps, bye, Uli
----------------------------------------------------------------
Ulrike Sattler RWTH Aachen (University of Technology)
Theoretische Informatik, Ahornstr. 55, D-52074 Aachen, Germany
Phone: +49/241/80 4566
Fax: +49/241/8888 360 u...@cantor.informatik.rwth-aachen.de