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