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.
There is no such assumption required, because we don't return a value in {BOTTOM} \cup Real, but in the disjoint union SUM({BOTTOM, Real}). That is, the return value is either of the form <<0, BOTTOM>> for failure or of the form <<1, x>> for success.
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.
Indeed. Could have phrased that better. All I meant is that if we do want to model the concept of a partial function in TLA+ for some reason, it is doable via that encoding.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/05d9dacb-4d7e-4223-b261-b9a908116bdd%40googlegroups.com.