[Date Prev][Date Next] [Chronological] [Thread] [Top]

**To**:**mizar-forum@mizar.uwb.edu.pl****Subject**:**Re: [mizar] A general question on writing recursive functions in mizar****From**:**trybulec <trybulec@math.uwb.edu.pl>**- Date: Sun, 04 May 2008 13:10:07 +0200
- Delivered-to: mizar-forum-outgoingx@mizar.uwb.edu.pl
- Delivered-to: mizar-forum@mizar.uwb.edu.pl
- In-reply-to: <B97B2420A93BA344915FAF6DFC08773F13C489@CEBREN.net.ttu.edu>
- References: <B97B2420A93BA344915FAF6DFC08773F13C489@CEBREN.net.ttu.edu>
- User-agent: Mozilla/5.0 (Windows; U; Win98; en-US; rv:1.7) Gecko/20040616

provides info on

1) the distinction between mizar functors and functions,

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.

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

Regards, Andrzej

- Prev by Date:
**[mizar] question about dependence operator in mmlquery** - Next by Date:
**Re: [mizar] question about dependence operator in mmlquery** - Index(es):