Re: Re: R: PVS GPLed

On Mon, 15 Sep 2008, Jesse Alama wrote:

> Freek Wiedijk <[email protected]> writes:
>
>>> By the way, what do you mean by 'old style "from"'?
>>
>> Nowadays to use a scheme you need to define predicates
>> and/or functors that match the arguments of the scheme using
>> "defpred" and "deffunc".  Mizar used to be able to figure
>> out by itself what the instantiations of the predicates and
>> functors in the scheme were just by looking at the shape
>> of the formulas.  I liked it that way.
>>
>> I'm sure that sometimes it was ambiguous, and that the
>> implementation of _how_ it worked was a big mess.  But in
>> practice it worked well for me, and I miss my proof looking
>> clean, without all the "defpred" noise.  When presenting
>> Mizar in a talk this is often one of the things that makes
>> my examples less convincing.
>
> I'm surprised that this feature would be taken out.  What's the reason
> for that?  I hate to ask a rhetorical question, but isn't one of the
> goals of the mizar language to be as close as possible to informal
> mathematical vernacular?  Shouldn't the direction of development be
> toward a richer language and/or more automation?

I think the reason actually was "more automation" and "richer language", 
but in a different part of Mizar (adjectives, and their automated 
mechanisms). I think it became increasingly difficult to have such 
new features implemented also in the higher-order matching module, and the 
solution was to drastically simplify it (at a price of requiring the 
authors to provide the instantiations explicitly). Using "defpred" was not 
the only possible syntactic solution, it could be done e.g. by a syntax 
like:

"... from MyScheme(A1,A2) applied to f(g(X)),...;"

(in cases where it is practical).

> But it
> would be nice if mizar also supported a less explicit argumentative
> style.

I am totally in favour of this (and many other experiments), we just need 
someone to implement it :-).

Josef