Re: [tlaplus] TLA+, Event B comparison

On Mon, 6 Jan 2020 at 02:28, Leslie Lamport <tlaplus.ll@xxxxxxxxx> wrote:

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.)

I wasn't clear in my previous comment. I was not suggesting the lifting construction as an operator in TLA+. My point was that partial functions can be modelled as a particular kind of total function (the lifting construction describes how). Should we adopt such a definition of partial function then the untyped nature of TLA+ becomes a non-issue.

Disclaimer, my TLA+ writing skills are a bit rusty. But just to illustrate what I meant,

(* disjoin union *)

SUM(A,B) == ({0} \X A) \cup ({1} \X B)

INJ0(a) == <<0,a>>

INJ1(b) == <<1,b>>

(* introducing the possibility of failure *)

BOTTOM == CHOOSE x: TRUE

UNIT == {BOTTOM}

PDOM(A) == SUM(UNIT, A)

FAIL == INJ0(BOTTOM)

SUCCESS(a) == INJ1(a)

(* partial functions are total functions with an added failure element *)

PARTIAL(A,B) == [A -> PDOM(B)]

(* domain of definition of a partial function *)

def(f) == {a \in DOMAIN f: f[a] # FAIL}

(* partial composition `f after g` *)

pc(f,g) == [x \in DOMAIN(f) |-> IF x \in def(f) THEN g[f[x][2]] ELSE FAIL]

(* example sqrt partial function on naturals *)

sqrt[n \in Nat] ==

LET candidates == {i \in 0 .. n : i * i = n} IN

IF candidates = {} THEN FAIL ELSE SUCCESS(CHOOSE i \in candidates: TRUE)

(* def(pc(sqrt, sqrt)) = {0, 1, 16, ...} *)

Nothing special here. Just the usual "monadic" approach to partiality.

Also to be clear, in the above I didn't mean to claim partial functions should be provided. But only that the language being untyped isn't necessarily an issue if all we want is some abstraction for partial functions.

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?

True, good point.

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.

--
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/09c58c33-2c74-4720-8343-8bae2dba3baa%40googlegroups.com.