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

*From*: Jorge Adriano Branco Aires <jorge.adriano@xxxxxxxxx>*Date*: Tue, 7 Jan 2020 01:37:10 +0000*References*: <46345329-ae57-41b5-8e55-f0dd23d71a0b@googlegroups.com> <1D262017-74FF-45BD-AD44-2550E5E0BDAB@gmail.com> <F1D32462-7E1B-4342-A8A4-97F17A38878C@gmail.com> <30ac153e-9b49-411c-bacf-c76d1b8b4050@googlegroups.com> <CAB3X38icefqKNg3mKwqG4Fqes+FBVT7MJX_QNQJc+XYrAON7CA@mail.gmail.com> <09c58c33-2c74-4720-8343-8bae2dba3baa@googlegroups.com>

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

I believe theliftoperator you want can be defined by choosing somevalue, 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'vemanaged 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 candefine mathematically. As someone has said, a work of art is finishednot when there is nothing else to add, but when there is nothing elseto remove.

And by the way, I didn't know that TLA+ includes syntaxfor projections. Has something been added to the language when Iwasn'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 onwhich it's defined, so "partial function" is meaningless. In typed languages, a function is definedto have a domain type, and a partial function is one that is not necessarily defined on all elementsof that type. Since TLA+ is untyped, it adopts the mathematical definition of a function and hasno 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.

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/CAB3X38gkjjOaAMQBTp53qT4T5LSSm-1Rd4VHdM6BaoxMQQTT9w%40mail.gmail.com.

**Follow-Ups**:**Re: [tlaplus] TLA+, Event B comparison***From:*Leslie Lamport

**References**:**[tlaplus] TLA+, Event B comparison***From:*Adriano Carvalho

**Re: [tlaplus] TLA+, Event B comparison***From:*Stephan Merz

**Re: [tlaplus] TLA+, Event B comparison***From:*Michael Leuschel

**Re: [tlaplus] TLA+, Event B comparison***From:*Leslie Lamport

**Re: [tlaplus] TLA+, Event B comparison***From:*Jorge Adriano Branco Aires

**Re: [tlaplus] TLA+, Event B comparison***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Zero Distinct States in TLC results?** - Next by Date:
**Re: [tlaplus] TLA+, Event B comparison** - Previous by thread:
**Re: [tlaplus] TLA+, Event B comparison** - Next by thread:
**Re: [tlaplus] TLA+, Event B comparison** - Index(es):