"Partial" Functions
Leslie Lamport
This is in response to the posting Dictionary type, but I thought
it merits a new topic.
Ordinary mathematics has no formal notion of a "partial function".
Mathematicians sometimes informally talk about a function that's not
defined on its entire domain. For example, they may talk about the
reciprocal function, which maps a number r in the set Real of real
numbers to 1/r, as a function on the set Real that's undefined on 0 or
"has a singularity at" 0. Formally, this just means that the domain
of the function is Real \ {0}.
The formal notion of a partial function arises in typed formalisms
with simple types. If the type system isn't expressive enough to
treat Real \ {0} as a type, then reciprocal must be defined to have
type [Real -> Real] that is a partial function because it's not
defined on all values of type Real. Since the customary formalism
of ordinary math doesn't use types, "partial function" has no
formal meaning.
Informally thinking of reciprocal as a function on Real that's not
defined on 0 may be useful. However, I see no benefit in thinking of
elements of DictionaryType as partial functions on STRING, when their
domain is such a "small" subset of STRING. You should be comfortable
with the idea that the domain of a function can be any set. No
mathematician would think of the element
[key1 |-> "value1", ..., keyN |-> "valueN"]
as a function on STRING that's undefined on any string in
STRING \ {"key1", ... , "keyN"}
You are better off learning to think like a mathematician. You can
formally define the reciprocal function to be either a function in
[Real \ {0} -> Real] or else a function in [Real -> Real] that maps
0 to some special value such as
NotANumber == CHOOSE n : n \notin Real
Either choice is fine. Depending on the nature of your spec, one
might be more convenient than the other. (As a more realistic
example, when specifying an algorithm, you might want to define
a function cdr on some set of sequences by
cdr[s] == IF s = << >> THEN nil ELSE Tail(s)
for a special value nil.)
By the way, in ordinary math, the two definitions of DictionaryType
that Dominik gave would be equal, since functions are defined to be
sets of ordered pairs and [S -> T] equals S \X T. TLA+ does not define
functions in terms of ordered pairs, the way mathematicians do,
because it's convenient to define an ordered pair (and any tuple) to
be a function. I could have defined a different type of pair--for
example by defining
Pair(a, b) == {{a}, {a, b}}
and defining [S -> T] to equal
{Pair(t[1], t[2]) : t \in S \X T}
Perhaps I should have done that, since it would have made f \cup g
a useful construct when (DOMAIN f) \cap (DOMAIN g) is empty.
However, instead I chose to make function-related operators like
DOMAIN primitives specified by axioms.
Leslie
fl
Ordinary mathematics has no formal notion of a "partial function".
Leslie Lamport
Bourbaki in 1939:
relation between a variable element x of E and a variable element y of
F is called a functional relation in y if, for all x \in E, there
exists a unique y \in F which is in the given relation with x. "We
give the name of function to the operation which in this way
associates with every element x \in E the element y \in F which is in
the given relation with x, and the function is said to be determined
by the given functional relation. Two equivalent functional relations
determine the same function."
as the "ordinary" definition of a function with domain E, except that
for no good reason it introduces a set F that's a superset of the
range. This is very strange, since it clearly fails to capture the
way mathematicians use the term function. For example, mathematicians
generally consider the reals to be a subset of the complex numbers,
and therefore consider a real-valued function to be a special case of
a complex-valued function. However, with Bourbaki's 1939 definition,
a real-valued function cannot be equal to a complex-valued function.
edition, and it is consistent with that definition being the same as
the 1939 definition. But, it is possible that they changed the
definition. I don't have a copy of that volume of Bourbaki.
as one component, thereby introducing a formal notion of "partial
function", would not be inconsistent with informal mathematical
terminology. For example, a mathematician say that "complex
functions" is the theory of complex-valued functions whose domain is
the set of complex numbers. Those "functions" are actually partial
functions because they are undefined at their "singularities". On the
other hand, they wouldn't consider a function on the real line to be
such a function, even though it is also a partial function with domain
the complex numbers.
function in a book written by a mathematician (not a computer
scientist) other than simply a set of ordered pairs having different
first elements. And I was educated as a mathematician. Hence, my use
of the term "ordinary" definition. If the current Bourbaki "Theorie
des Ensembles" introduces a concept of partial functions, then I will
abandon that term. I hope someone who has a copy will tell us what it
says.
fl
I hope someone who has a copy will tell us what it says.
D. Couturier
I sent a mail to Leslie Lamport about this topic. He kindly asked me to post our messages.
____________________________________________________
I read the thread "Partial Functions" on the TLA+ Google group. Hereunder is my account about this subject.
First of all I am an engineer, not a mathematician.
In France, during all my education after the elementary school, from the age of 11 in 1969 to the age of 23 in 1981, I was taught "mathématiques modernes" (http://fr.wikipedia.org/wiki/Mathématiques_modernes <http://fr.wikipedia.org/wiki/Mathématiques_modernes> ), in the direct line of Bourbaki.
There was a clear difference between "une fonction" (a function) and "une application" (a total function). When we studied a function, the first thing to do (the first question of the exercise) was to define the "domaine de définition" (domain) of the function.
I retrieved my course notes from my first year post high school (I was in class of "mathématiques supérieures" - http://en.wikipedia.org/wiki/Classes_Préparatoires <http://en.wikipedia.org/wiki/Classes_Préparatoires> ).
--------------------------------------------------------------------------
Definitions.
Let E and F be sets.
. A graph is a sub-set of E \x F.
. A "relation" (binary relation) between E and F is a triple (E,F,G) where G is a graph from E \x F.
. A "fonction" (function) f is a "relation" (E,F,G) for which the following
holds: if (x, y) \in G and (x,y') \in G then y = y'.
. The "domaine de définition" (domain) of a function f is D(f) = {x \in E: \E y \in F : (x,y) \in G}
[In France, we use \E! for "there exists one and only one"]
Property
For each "fonction" (function) there is a related "application" (total function).
[Today I realize that "the" related one was the one with the "biggest" domain.]
----------------------------------------------------------------------------
According to the above property, we used (teachers and students) the word "fonction" for "application", except when the difference of meaning mattered.
I know you can read French:
http://fr.wikipedia.org/wiki/Application_(mathématiques) <http://fr.wikipedia.org/wiki/Application_(mathématiques)> (especially section 1).
Yours faithfully,
Dominique Couturier
____________________
Dear Dominique,
[...]
Thanks for the information. So, suppose you proved a theorem in a class on real-valued functions, and in a class on complex-valued functions you had a function f with f(x) a real number for all x in its domain. You then couldn't have applied to f any of the theorems you proved in the earlier class were for functions (E, F, G) with F the set of reals and f has F equal to the set of complex numbers. I wonder why people make so unnecessarily complicated. Did you ever encounter any occasion in which adding the E and F to the definition of a function was helpful? In any event, I will use the term "simple" instead of "usual", since \ simplicity seems to be unusual in this world.
[...]
By the way, I'm curious: What were you taught was the meaning of f(x) when x is not in D(f)? If the answer was "you weren't allowed to write it", then that would mean you couldn't write \A x : (x \in D(f)) => P(f(x)) for some predicate P.
Cheers,
Leslie
______________________
Dear Sir,
[...]
4/ What were you taught was the meaning of f(x) when x is not in D(f)?
Remember that if you write f(x), implicitly f is a total function and x \in D(f). So you were not allowed to write tan(pi/2). If ever you wrote it on the blackboard, the teacher would probably cry out: Horreur ! Get out of my classroom at once!
5/ Paradoxically, it doesn't mean we couldn't write \A x : (x \in D(f)) => P(f(x)). Because if x \in D(f) is false, we do not need to "evaluate" f(x) : (false => M) is true whatever the value of M, then (x \in D(f)) => P(f(x)) is true.
It was not an explicit rule given to the students, but I think all of us thought this way.
I think we used (without realizing what we did) kind of 'moderate' interpretation of logic, as you call it in your book "Specifying Systems".
You know, formal logic was not the main concern of Bourbaki!
6/ Do remember that I am not a mathematician, and I was in "maths sup" 37 years ago.
Yours faithfully,
Dominique Couturier
________________________
Hi Dominique,
[...]
>4/ What were you taught was the meaning of f(x) when x is not in D(f)?
>
>Remember that if you write f(x), implicitly f is a total function and x \in D(f). So you were not allowed to write tan(pi/2). If ever you wrote it on the blackboard, the teacher would probably cry out: Horreur ! Get out of my classroom at once!
>5/ Paradoxically, it doesn't mean we couldn't write \A x : (x \in D(f)) => P(f(x)). Because if x \in D(f) is false, we do not need to "evaluate" f(x) :
(false => M) is true whatever the value of M, then (x \in D(f)) => P(f(x)) is true.
>It was not an explicit rule given to the students, but I think all of us thought this way.
>I think we used (without realizing what we did) kind of 'moderate' interpretation of logic, as you call it in your book "Specifying Systems".
Well, I’m glad you were using what I regard as the simple, natural way to interpret something like 1/0: it’s some unspecified value, which might equal 42 or the set of quaternions or anything else. Some people think it should have a special non-value “undefined”, which leads to the complication of having to deal with three-valued logic.
>You know, formal logic was not the main concern of Bourbaki!
I know they were mathematicians, and formal logic isn’t the main concern of mathematicians. However, I thought that they wanted to build all of math from axioms and definitions, and they wanted it to be rigorous. You can’t avoid this issue if you do that. However, you can avoid mentioning it. I suspect that their attitude was that they never discussed meaning. Math is just a set of rules that tells you how to prove things about well-formed (syntactically correct) formulas. Since 1/0 \in Reals is a well-formed formula, you can ask whether you can prove it from the axioms. There’s a problem only if the axioms aren’t sound, which means you can prove FALSE. Engineers aren’t satisfied with that view of math (and I expect mathematicians aren’t satisfied with it either, but they were when I was in school), so I felt obliged to write that section oo “silly formulas”.
[...]
Leslie
_________________