- From: Christian de Sainte Marie <csma@ilog.fr>
- Date: Tue, 24 Jul 2007 15:03:35 +0200
- To: Michael Kifer <kifer@cs.sunysb.edu>
- CC: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>
Michael Kifer wrote: > > 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. Still struggling: can you confirm or explain away for me the following assertions, please? - in BLD, the same symbol in Const can have multiple signature (e.g. i and f0 and fn and pm)? - in BLD a signature can contain at most one signature expression? - not all symbols in Const have signature i{} (that is, some symbol in Const have only fn and/or pn signatures)? Thanx, Christian
Received on Tuesday, 24 July 2007 13:04:05 UTC