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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Thu, 2 Jan 2020 12:25:58 -0800 (PST)*References*: <46345329-ae57-41b5-8e55-f0dd23d71a0b@googlegroups.com> <1D262017-74FF-45BD-AD44-2550E5E0BDAB@gmail.com> <F1D32462-7E1B-4342-A8A4-97F17A38878C@gmail.com>

A minor correction to Michael's post.--in particular, to this statement

-- Functions in TLA+ are total, while B supports relations, partial functions, injections, bijections, etc.

I believe a partial function is usually said to be a function that is not necessarily defined on all

elements of its domain. In math, the domain of a function is by definition the set of elements on

elements of its domain. 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.

Mathematically, a relation on a pair S, T of sets is a subset of S X T. By "supporting" relations,

injections, etc., Michael means that B provides a large collection of arrow symbols that express certain

injections, etc., Michael means that B provides a large collection of arrow symbols that express certain

sets (more precisely, types) of relations on pairs of sets. For example S -some-kind-of-arrow-> T

might define the set of all relations R on S, T such that (s1,t) and (s2,t) in R implies s1=s2.

Abrial liked those operators and apparently used them frequently when writing specs.

Operators corresponding to all those arrow symbols are easily defined in TLA+. I occasionally

wrote specs that needed to define a set of relations on some pair of sets, and writing that set of

relations as S -some-kind-of-arrow-> T would have been nice. However, they were not always

the sets of relations defined by the B arrows. I thought about providing a few user-defined

arrow symbols for the purpose in TLA+, but I decided they weren't useful enough. Apparently Abrial

arrow symbols for the purpose in TLA+, but I decided they weren't useful enough. Apparently Abrial

and I wrote different kind of specs. Most of my specs were for concurrent systems; he designed

B for specifying sequential programs. Or perhaps we just had different tastes. I think he

found the use of all those arrows elegant, while I found it confusing.

Leslie

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/30ac153e-9b49-411c-bacf-c76d1b8b4050%40googlegroups.com.

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

**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

- Prev by Date:
**[tlaplus] In the Composition Rule from section 10.2 of Specifying Systems, what is F_ij?** - Next by Date:
**[tlaplus] Question regarding Two Phase Commit spec and the enabling condition of one of its definitions** - Previous by thread:
**Re: [tlaplus] TLA+, Event B comparison** - Next by thread:
**Re: [tlaplus] TLA+, Event B comparison** - Index(es):