I believe your proposal is to represent a partial function in TLA+ as one having a special value
Bottom in its domain. However, that means that to talk about partial functions on, say the real
numbers, one would have to add an assumption that Bottom is not a real number. Perhaps some
people find partial functions useful enough to add such an assumption for every set on which
they want to define a partial function. The alternative would be to modify the semantics of
TLA+ to add Bottom as something other than a value--analogous to adding a truth value "undefined"
to turn ordinary logic into three-valued logic. This would require modifying the definitionof every primitive TLA+ operator to specify its value when one or more of its arguments is Bottom.
(I wonder if 2 = Bottom should equal FALSE or Bottom.) I see no reason to do this to support a
concept I find to be useless.
Your remark about the untyped nature of TLA+ becoming a non-issue implies that it is now an
issue. I trust that you were talking only about it being an issue for dealing with partial
functions. The general question of whether being untyped is an "issue" is best discussed
off this forum.
Leslie