Re: Comments on v0.96 Section 1-4.2

[Michel.Bidoit@lsv.ens-cachan.fr (Michel Bidoit)]

Dear All,

Just a word to strongly support the point made by Maura:

>> Let-in ???
>> I think that in Paris we decided to have in (that is: to propositively add
>> it to) the new summary a construct to have shortcuts for long terms to be
>> used in axioms, something like
>>   let t=f(hgfhf(jjj,yuyt,sdfdsf,........) in
>>   t=g(t,t)=>p(t,f(t))
>> whose semantics is expected to be "to add to the local environment a
>> partial constant t of the expected sort and the axiom t=.... and use it to
>> evaluate the axiom, discharging then the constant".
>> 
>> I didn't find any trace of this in the summary.
>> Is this because
>> a) my memory is not anymore as it used to be ;-)
>> b) some different decision was made afterward,
>> c) we leave it to the concrete syntax (...?...I dislike to have a concrete
>> construct that cannot be mapped into any abstract one, as we don't have
>> local declarations in basic items)
>> d) I simply missed it?
>> 
>> [My notes from the Paris meeting tell me that we concluded (on Sunday
>> morning) by agreeing that it was more in line with algebraic
>> specifications to introduce a (local) constant and and define it by an
>> axiom, cf. the treatment of if-then-else or cases by conditional
>> axioms.  If my notes are inaccurate on this point, kindly let me know.
>> --PDM]
>> 

While I am sure that Peter's comment reflects accurately what happened
in Paris/Lille, I share Maura's view that local values in formulae are more
than useful. BTW local constant declarations are certainly not enough, at
least functions would be needed to replace this, and anyway in my view they
are not as convenient as "let-in".

Best regards,
Michel
PS: I basically also agree with all other points made by Maura...