# Re: function symbols in SWRL FOL

From: Enrico Franconi <franconi@inf.unibz.it>
Date: Sun, 5 Dec 2004 14:19:19 +0100
Message-Id: <452AC781-46C0-11D9-80CA-000A9575BDDE@inf.unibz.it>

To: Sandro Hawke <sandro@w3.org>
```
On 25 Nov 2004, at 14:24, Sandro Hawke wrote:
>> Secondly, when we have equality (as we do in SWRL FOL), function
>> symbols do not add to the expressive power of the language as we can
>> easily substitute "functional" predicates. I was hoping to refer you
>> to a suitable logic text book at this point, but one didn't
>> immediately come to hand so I will attempt to DIY it. To make a
>> predicate f "functional", we simply add:
> ...
>
> Can we characterize this transform in a few more regards?
>
> 1. The models of the pre-transform formula (F1) and the post-transform
> formula (F2) are the same.

They are not. The transformation preserves the functionality, not the
definition of the function. So, the models of F2 will be many more and
will include the models of F1. So, functions symbols do increase the
expressive power of the language.

> 2. It is lossy / not reversable. You can't look at F2 and figure out
> what F1 must have been.

Yes, it is lossy.

> 3. For many computational logic systems, the performance
> characteristics of operating with F1 will be significantly different
> from those of operating with F2. (Where "significantly" is perhaps
> extraneous, because theorem provers seem to be extremely sensitive to
> syntactic transformations.

This is not clear. I suspect that since the encoding requires equality,
there may be fragments of the logic in which it is more efficient to
reason with built-in functions rather that equality - but this is just
a guess.

> The other half of the puzzle is about the transform between n-ary
> predicates and binary predicates (which I wish we could agree to call
> dyadic predicates, since the word "binary" has such strong other
> associations). There is a transform which effectively converts n-ary
> to 2-ary predicates, but it is not perfectly model-preserving, since
> it reifies the relationship.

Depending on the language (which shouldn't be too expressive),
reification of n-ary relations may preserve satisfiability and logical
implication, even if it does not preserve models (see, e.g., [1]).
So, there is a sense in which you can say that reification is not lossy.

[1] The Description Logic Handbook: Theory, Implementation and
Applications. Cambridge University Press, 2002. Section 5.4.1
("Reification of roles"), and Section 5.7 ("Relations of arbitrary
arity").

cheers
--e.

Enrico Franconi                  - franconi@inf.unibz.it
Free University of Bozen-Bolzano - http://www.inf.unibz.it/~franconi/
Faculty of Computer Science      - Phone: (+39) 0471-016-120
I-39100 Bozen-Bolzano BZ, Italy  - Fax:   (+39) 0471-016-129
```
Received on Sunday, 5 December 2004 13:19:56 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:46:18 UTC