[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+, Event B comparison

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 definition
of 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.


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.