Re: [mizar] Proposal for binders in Mizar

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

Hi Freek,

> I have written a short note with a proposal for a _syntax
> for binders_ in Mizar (which I think is one of the things of
> which I think that it would improve Mizar most):
> 
> http://www.cs.kun.nl/~freek/notes/binder.ps.gz
> 
> Maybe it's useful to have a discussion about this?

Yes, let's hope for more than just discussion :-).

Some very technical remarks:
- It would help me, if you used "F" instead of "f" for a scheme-like 
  function specifications, I became a bit confused at p. 4, where "f" is 
  also used for the FinSequence
- Why allow only one "lambda" argument? Why not have "binder x1,...,xn", 
  when F takes n arguments?

More serious remarks:
- It seems to me, that you do not give the full semantics of the 
  construct, I can just try to figure it out from the examples. Maybe it 
  is something obvious to people working with higher order systems, but 
  could you state it explicitly? Otherwise it is hard to think 
  generally of the correctness conditions, that the system should check, 
  when introducing such definitions, and also the automatisms that could 
  be implemented. 

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

- The (semantically) interesting case is, when F cannot be expressed on 
  the object level. E.g. "F(Nat) -> Real" can be expressed as 
  "f being Function of NAT, REAL", so binder is just a new functor taking 
  f as an argument, while "F(set) -> set" (e.g. F = Card) cannot, so 
  binder brings some new expressive power over classes in this case.
  E.g. currently we can define the class (functor) Alef using e.g. the 
  class (functor) Card, but you must name all such classes, and if we 
  wish, the definition expands to a first-order set theoretical formula.
  What you suggest, means that it will no longer have to be so, you will 
  generally have binder Foo taking any (function-like) class to another, 
  so actually a mapping between formulas. 
  This becomes probably more visible, if we allow binders for predicates 
  too, e.g. 
  "{ P[set] }; binder y at x of P[y] means P[Card(x)] or Blah[x];",
  so actually you can also say:
  "{ P[set] };
   binder Separation y at A of P[y] means 
   ex X being set st for x being set holds x in X iff x in A & P[x];",
  so we get schemes of assertions (not just of theorems like the current 
  schemes).

- I am not sure that this is (now) needed at its full strength, a lot of 
  things would be better if we just fixed the behavior of the Fraenkel 
  operator (and terms) to be more aware of the types involved.
  So e.g. your "lambda" definition is st. like
  { [x, x^2 + 1] where x is real number} and we only need the system to 
   notice that this defines a function and the typings - that it is a 
  Function of REAL,REAL. 
  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.
  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. Also the implementation within current system should be quite 
  cheap (just enhance analysis of Frankel terms and implement the lambda 
  sugar).

Best, 
Josef