[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Re: R: PVS GPLed



On Mon, 15 Sep 2008, Jesse Alama wrote:


Freek Wiedijk <freek@cs.ru.nl> 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