Re: [mizar] Proposal for binders in Mizar

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Freek,

> >- Why allow only one "lambda" argument? Why not have "binder
> >  x1,...,xn", when F takes n arguments?
> 
> I couldn't think of a good example where this would be
> benificial.  Also, each xi should go with an "at ..."
> parameter, and I thought it would become clumsy.

Well, e.g. the "lambda" binder - it does not use the "at" parameters at 
all. 

> >- It seems to me, that you do not give the full semantics of
> >  the construct,
> 
> Surprisingly I hadn't given this any thought: I had only
> thought about the syntactical aspects.
> 
> But I think that one way to "model" this is by saying that it
> introduces a new function symbol for every different instance
> of the binder.  So for instance with sum binder, you should
> imagine that there is a separate symbol "sum_f" for every f().

I sse. I was also a bit puzzled by the intended meaning of the "lambda" 
variables in the binder definition, but now it seems to me that they are 
there just to define the syntactical pattern of the binder, and cannot be 
used in its definiens. You can only use the "at" variables there, right?
This is a bit new, since in normal definitions, you are supposed to use 
pattern variables in the definiens.

So the general format of the definiens is st. like 
P[at_args,it(at_args),F(at_args)], 
(actually "equals" definition could also be possible), and we need to 
check the existence (and typing) and uniqueness, so e.g.
for at_args ex x (being ...) st P[at_args,x,F(at_args)], etc.

> So how do you treat schemes in your first order translation?

They are omitted in the first version, which causes that some reproval 
problems are not exported. In the second version (not published yet), they 
are being instantiated each time they occur. This is pretty bad, but 
enough for the completeness of the reproval task. Obviously, if you want 
to prove something new (which should be one goal of the translation), this 
can cause troubles. 
It seems to me, that it is not completely unrealistic, to think of having 
e.g. Separation integrated as an inference rule into first-order ATPs, 
which could give a lot. I am not sure about the rest of schemes - you 
reaaly need only Replacement ( or even nothing if you use NBG) - but it is 
a matter of convenience and length of proofs.

> >  if we allow binders for predicates too, e.g. 
> 
> I thought about this, but I don't see the use of this,
> really.  Do you have a good example from mathematical
> practice?

As I wrote, I am not a big fan of this, but yes: You could e.g. first 
define Separation as a scheme of assertions and then prove it as a normal 
scheme. Maybe there are some set-theoretical principles formulated like 
"for each formula" (things like Levy's Reflection come to mind) that could 
be formulated this way, but I prefer to see them the way they are done now 
(i.e. formalizing the language and axioms of ZF, etc. inside Mizar), 
though it may become necessary to have such things in the future.

> >  Once we have "lambda" working, there is not much need for
> >  other binders:
> >  (integral lambda y of y to_power n).x = (x to_power (n + 1))/(n + 1)
> >  (Partial_Sums lambda y of y).n = n*(n + 1)/2
> >  lim(lambda y of y^2, a) = a^2
> >  etc.
> 
> I'd much rather write "sum i at 1,n of f(i)" than "(sum
> lambda i of f(i)).[1,n]".  Especially the "lambda" is ugly.
> So if you would implement this approach I'd much prefer to
> have a symbol for the lambda (maybe "\" after all? then it
> the example would become "(sum \i of f(i)).[1,n]"), instead
> of a keyword.

I was just interested in the semantics, I have no problem with "\" instead 
of "lambda", or even more syntactic sugar like the "at" construct.

> >  Obviously, this approach is weaker than your suggestion,
> >  because it requires the lambda function to be a set, but
> >  (except from weird individuals writing strange
> >  set-theoretical stuff :-) this should not hurt much.
> 
> No, that wouldn't hurt at all, I think.  So this solution
> would be much closer to what one finds in other systems.  But
> to me it feels "less Mizar-like"...

Maybe you are right, I don't know. I just do not like the current lack of 
typing for the Fraenkel terms, and fixing it is also a way how to get some 
of these features.

Best,
Josef