Re: [tlaplus] TLA+, Event B comparison

I believe the lift operator you want can be defined by choosing some

value, lets call it Bottom, and writing:

lift(f,a) == [x \in a \union DOMAIN f |->

IF x \in DOMAIN f THEN f[x] ELSE Bottom]

But I don't know why I would ever want to use such an operator. (I've

managed to get along for well over 50 years without it.)

TLA+ could include syntax for disjoint unions and anything else you can

define mathematically. As someone has said, a work of art is finished

not when there is nothing else to add, but when there is nothing else

to remove. And by the way, I didn't know that TLA+ includes syntax

for projections. Has something been added to the language when I

wasn't looking?

Leslie

On Sunday, January 5, 2020 at 3:32:32 PM UTC-8, Jorge Adriano Branco Aires wrote:

Just a small observation regarding partial functions.

In math, the domain of a function is by definition the set of elements on
which it's defined, so "partial function" is meaningless. In typed languages, a function is defined
to have a domain type, and a partial function is one that is not necessarily defined on all elements
of that type. Since TLA+ is untyped, it adopts the mathematical definition of a function and has
no need for anything like a partial functions.

Indeed the classical definition of partial function doesn’t fit an untyped framework like TLA+. That however does not imply partial functions can’t be modelled in an untyped framework. They can. The classical construction for that purpose would be the lifting of partial functions f: A->>B to total functions lift(f): A -> 1 + B. Here "+" represents disjoint union, 1 represents some singleton, and lift(f)(a) = * (left injected) if f undefined in a, and lift(f)(a) = b (right injected) otherwise.

TLA+ could include syntax for disjoint unions, injections, cotuples, much like it includes for products, projections and tuples. And TLA+ could define syntax and operators for partial functions modelled as the corresponding lifting. Whether these are worth including or not is then a matter of design choice and personally taste.

J.A.