Re: [mizar] Proposal for binders in Mizar

[Freek Wiedijk <freek@cs.kun.nl>]

Hi Josef,

Thanks for your comments!  To answer some of your points:

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

I tried to keep the proposal simple.  For instance, I could
also have allowed for a "P[...]" parameter, for instance for
the sum over primes example.  But I thought this would be
good enough, as I could do the example without it, and so I
left it out.

>- 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().

It's similar to the schemes: there if a scheme takes a
parameter f() I don't imagine the thing to quantify over
those f()'s, because it wouldn't denote anything in the set
theory.  Instead I always think about it as a uniform way to
prove a whole collection of theorems.

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

>- Are binder terms allowed to match scheme-like functor
>  specifications?  I.e., does "sum i at x of F(i)" match
>  "G(natural number) -> complex number"?  So "sum i at n of
>  (sum k at i*n of F(k,i))" is possible?

Yes, that's the idea.

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

>  Maybe the "lambda" could be just a very simple syntactic
>  sugar, like:  "lambda x of x^2 + 1 [qua Function of
>  REAL,REAL]" which actually just expands to that Fraenkel
>  and gives the system the hint for the preferred typing.
>
>  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.

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

Freek