Re: [mizar] Binders?

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

On Mon, 14 Oct 2002, Freek Wiedijk wrote:

> (Of course if you have lambda abstraction, _then_ the first
> is just an instance of the second.  But Mizar hasn't, not in
> a way that makes this "binder" notation look nice (or has it?))

I would vote for having lambda notation, or at least for having a serious 
discussion about it. The usage of the Lambda schemes to get Functions is 
often clumsy (maybe because the scheme implementation is quite 
type-hierarchy unfriendly). This does not mean I suggest lambda calculus, 
by no means. Just to extend the current "lambda notation" given by 
deffunc, to create "Function of ..." in situations when it is possible 
(i.e. the "Function of ..." is registered type). 

> Another argument for wanting binders is that it conforms to
> "normal" mathematical practice.  Mathematicians never write
> lambdas for functions (so they don't have lambda-binders),
> but they certainly write sum-signs that bind variables.

Exactly, let's avoid the word "lambda" at all (some people are a bit 
sensitive about it :-) ). "Normal" mathematicians rarely know, what lambda 
calculus is, however, they surely know, that "x |-> x^2" defines a real 
function for x being real.

Josef