[Date Prev][Date Next]
Re: [mizar] A general question on writing recursive functions in mizar
Ozyavas, Adem wrote:
provides info on
1) the distinction between mizar functors and functions,
the distinction is not specific for Mizar.
We use two different names for formula constructor (predicate) and the
similar set theoretic object (relation). Unfortunately there is no such
commonly accepted distinction in the case of functions. Usually we use
'function' for a set theoretic object and 'lingual function' for the
term constructor. The name 'functor' for the term constructor was
borrowed from Rasiowa&Sikorski "Mathematics of Metamathematics". A
little bit better that 'function'. Still, it should be not confused with
'functor' in category theory, that is a (specific) function.
The distinction is important, beacuse mixing two concepts may lead to
the inconsistency. E.g. we may define ther
union of two sets (a functor):
A \/ B
but there is no corresponding function (the domain cannot be the
Cartesian square of the set of all sets, because there is no such thing).
In concrete mathematics the distinction is not so important, but there
are stll technical issues described by Adam.