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

Thanx,

Christian

Received on Tuesday, 24 July 2007 13:04:05 UTC