- From: Michael Kifer <kifer@cs.sunysb.edu>
- Date: Tue, 24 Jul 2007 08:50:20 -0400
- To: Christian de Sainte Marie <csma@ilog.fr>
- Cc: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

> > Michael Kifer wrote: > > > >>- In 2.1.3, the remark that f() and f can be interpreted differently and > >>dialect may introduce axioms to make them equal should be clearly marked > >>as irrelevant to BLD (where symbol f has either signature f0 or i, but > >>not both). > > > > why is it irrelevant? > > I understood that, in BLD, the same symbol f can have either signature > i{} or f0{()->i}, but not both. And thus, in BLD, whether f = f() or not > is irrelevant. We wanted to make it clear that f=f() is not a tautology. It is not a matter of signatures. Even if f has the signature ...{i ()->i}, i.e., for f and f() are well-formed, neither f != f() nor f=f() is not derivable. However, in your rule set (if you allow equality) you can add an equality abc=abc(). Then in your ruleset abc=abc() will be derivable but cde=cde() will still not be derivable (unless you also add cde=cde()). This is what that remark says. > My point was only about separating more slearly what is BLD and what is > the more general framework in which BLD is defined. > > > > The problem is that if we do not use signatures then we have to split the > > set of symbols into subsets. > > You mean, subsets like "function" (or even "x-ary function"), predicate, > etc? If yes, ok, I get your point. Yes, function (for different arities), predicate (for all arities), individual. We first tried to use those categories of symbols, but then realized that this has problems with extensibility. --michael

Received on Tuesday, 24 July 2007 12:54:25 UTC