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

Re: [tlaplus] TLA+, Event B comparison



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.

--
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/CAB3X38icefqKNg3mKwqG4Fqes%2BFBVT7MJX_QNQJc%2BXYrAON7CA%40mail.gmail.com.