Re: [BLD] Signatures (BLD 7/20)

> 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)?

Ah, sorry. I forgot about it. Yes, in the basic logic f=f() cannot even be
a well-formed formula.

The piece of text we are talking about was kind of important for the old
logic where we allowed symbols to be polymorphic. It is also important for
extensions, but not for BLD. You are right!

Sorry for propagating this confusion.


	cheers
	  --michael

Received on Tuesday, 24 July 2007 15:39:18 UTC