TLA+ to Wombat2 correspondence

  I looked at TLA+ a decade or so ago and didn't grok it. I looked at the wrong sort of documentation. This time I looked at Lamport's "science" technical document: https://lamport.azurewebsites.net/tla/science.pdf. Surprisingly TLA+ has a lot of similarities to Wombat2. Here is the approximate correspondence.

1. TLA+ Sets correspond to Types

In Wombat2 there is a lattice hierarchy of types that make them behave quite like sets. In TLA+ there are no types, but the way he uses sets, such as the set of Integers, corresponds closely to wombat2 types.

Lamport also claims that "everything is a set" using the ZF (Zermelo-Frankel) system. So 3 is a set, and maybe 2 is an element in 3. Such nonsensical questions don't arise in Wombat2. Yes, you could use ZF as the implementation of natural numbers, but that doesn't make properties of that implementation into properties of the type being implemented. This doesn't cause any conflict between TLA+ and wombat2 because TLA+ doesn't make any substantive use of this.

2. TLA+ mapping corresponds to Proc

On page 14 he talks of "mapping", giving * (multiplication) as an example that is defined for numbers. Since there is no type system to exclude non-numbers, we presume the mapping fails for non-numbers. And so this corresponds to Proc.

A mapping that always gives a boolean result is called a "predicate". This corresponds to a TProc(X,Bool). He gives "=" as an example, and in Wombat2 "==" is also defined for any pair of values.

3. Expressions and Formulas, meanings and interpretations

Numeric expressions using constants and arithmetic operations are distinguished from Boolean expressions, also called formulas. These exist in wombat2, of course.

Then on page 15 we see algebraic expressions and algebraic formulas. These have "variables" in them. Wombat2 reflection allows looking inside expressions. Identifiers and operators, which are compile time things, get converted to atoms which are runtime things. Wombat2 is more general, since Lamport is only talking about numbers. TLA+ writes the meaning of any of these with special (doubled) square brackets: ⟦exp⟧. Then an "interpretation" is a mapping from variable identifiers to values. In wombat2 the equivalent would be a record type mapping atoms to values. If ϒ is an interpretation in TLA+ then ⟦exp⟧(ϒ) is the value of the expression with that assignment of values to variables. Wombat2 can do something similar, but it is only in a part of the language not meant for ordinary programming.

Formulas are also similar to wombat2 proposition types. These are types that correspond to a a proposition, with a value of the type being a witness. 

4. Subsetting corresponds to subtyping (including refinement/subset types)

TLA+ { x∈X | F(x) }, for some formula involving x, corresponds in Wombat2 to X/{ F%($) } where F% is a Type expression with an input argument of type X, and where values of X are included if the generated type has a value (witness).

5. Mappings and Functions

In TLA+, mappings have 0 or more untyped arguments. The defining expression may be only valid for arguments from some "sets". Mappings can cover things that are too big to be sets. In wombat2 things too big to be types are in a higher universe, but I haven't worked out how that exactly works, but currently there is no similar distinction.

A function in TLA+ has one input, that can be a tuple, and one output, which can also be a tuple. So corresponds pretty well to TProcs in wombat2. Where TLA+ writes v∈S↦exp, that corresponds to {'S=>T: `v=$; exp }. Functions(=TProcs) are values just like numbers in TLA+ and wombat2.

6. Lists, Tuples, etc

TLA+ has lists (in angle brackets) that are "ordinal sequences. Ordinals are "first, "second", etc. So TLA+ has indices starting at 1 so that the second item is item 2. Then it has ordinal sequences that are meant for things that happen starting at time 0, so these are 0 based, and the entries are separated by right arrows: →. The latter seems to correspond to the semi-colon separator between effects in wombat2.

7. Rendering effect-based programs as mathematics

We then come to the parts of TLA+ that are used in proving things about programs. This is the stuff that wombat2 would like to learn from.

The first trick is to divide the execution into steps. Then each variable turns into an array of values, giving the value at each step. Then the execution of the program can be expressed as logical facts about how these variables have values at each step. Wombat2 has a start in this direction with the TimeOrder values marking the start and end of effectful expressions.

Logical operations in TLA+ are extended with "always" (▢) and "eventually" (◊) and "always eventually" and "eventually always".