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

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