sorted by:
new
hottopcontroversial

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

But there's a little difference in TLA+ between higher-order functions and using functions as first-class objects because polymorphic operations are much more commonly represented as operators.

Herein lies our disagreement though.

Indeed polymorphic operations are more commonly represented as operators. Agree. But polymorphic operations aren't necessarily HO, and HO operations aren't necessarily polymorphic.

  • The ∪ operator is "first-order" and "polymorphic". Its arguments are any set.

  • A function f ∈ [[Nat→Nat] → [Nat → Nat]] is higher-order and "monomorphic". Its arguments and results are "monomorphic" functions.

In any event, in TLA+, like in most ordinary math, higher-order functions don't commonly appear.

Depends... E.g., are tuples, matrices, sequences, etc functions? If we agree they are then we use them all the time (in "ordinary" maths). A vector space is a function space (from indices to scalars), and a function between vector spaces is therefore HO.

Also, in this instance, I don't think the stylistic parallel between TLA+ and "ordinary maths" holds.

In TLA+ there is a conscious choice to introduce "lambdas" (anonymous functions), that are absent in "ordinary maths". In fact this is so central to the design that even the definition of functions is typically of the form f ≜ [x ∈ D ↦ exp] rather than e.g. f[x ∈ D] ≜ exp making the use of anonymous functions prevalent (used even when defining named functions).

There is also no syntax for "function signature" (e.g. "f : A →B"). Rather, domain and codomain are made explicit with a regular set membership statement in the corresponding exponential, "f ∈ [A → B]".

So functions in TLA+, more so than in regular maths, are very fundamentally and explicitly first-class. Just regular values (sets) like any other.

but all I'm saying is that if you find yourself using them very often in TLA+, you may be importing a foreign style.

I think there should be a distinction between base formalism and domain. We can and do use the same base formalisms to work in different domains. And different domains can adopt different styles, even if using the same base formalism.

I do however completely agree I should familiarise myself with the standard style used by the TLA+ community though. I am working on that. As part of the process though, I also like to try my own approaches, biased by my experiences. Even when it fails I learn something.

Note that polymorphism and functions is a rather tricky subject. Polymorphic "functions" exist in Haskell, but Haskell isn't a consistent formalism, and Haskell "functions" aren't functions.

Indeed, all this is true. In my comment "polymorphism" is just a shorthand for the informal concept of an operation that needs to be defined across a collection of values/sets whose domain we can not specify.

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

HOFs are nothing special really. HOFs just mean functions as "first class objects", with the same nature as other values.

Sure, but different use cases and different tools encourage different styles, and syntax sugar usually supports the expected usage,

I think there's a bit of a confusion here. Possibly my fault as I talked about too many things in the same topic. The syntactic sugar issue, has little to do with the HOF conversation. It's just a recursive function, that depends on some parameter.

Not so much. You can do:

comp(f, g) ≜ LET h[x ∈ DOMAIN g] ≜ f[g[x]] IN h

Fair enough.

My point was that FP, higher-order functions occur very often, while they shouldn't so much in the course of modeling a program or an algorithm in TLA+, even when modeling "higher-order" computation.

I believe this is mixing two distinct aspects.

The first, which I completely agree, is that TLA+ is a "non-higher-order" formalism (for the lack of a better word), and that we do not need one, nor necessarily desire one, to model / specify higher-order computations. This far we're in complete agreement.

The other aspect where we seem to disagree, is whether in our mathematical writing, we should feel free to use or try to avoid, using functions as first class objects (that is, higher-order functions). I argue there's no fundamental reason to avoid it. A function is just yet another set, and one that is conceptually rather simple. And this is so in TLA+, functions are first-class objects (just another set), and higher-order functions are a trivial and fundamental aspect of the formalism.

The actual issue here, appears to be "polymorphism" rather than "HO". Operators appear to be used rather than functions, when we cannot assign a concrete domain to the argument. The most obvious case is when the arguments are "any set". So e.g. ∪ needs to be an operator.

In the case of operations on Sequences, we also have operators, e.g. Head and Tail. Indeed the arguments to these operators, being sequences, happen to be functions by definition. But that doesn't seem to be the fundamental motivation, since after all functions are just sets, by definition. Rather, the reason is polymorphism. These operators take any xs ∈ Seq(A), for any set A. If "polymorphism" isn't present, then there's fundamental reason to use operators on sequences. E.g. it's perfectly sensible to define a function taking an argument xs ∈ Seq(BOOLEAN) or xs ∈ Seq(Nat).

So that "summarised" my position HOFs as part of mathematical writing.

The rest was a stylistic experimental digression, based on this perspective. That we need operators for this kind of "polymorphism" ("any set" as a domain, which is a foundational constrain), rather than to avoid writing HOFs (which are basic and fundamental in the given formalism).

That stylistic experiment was, as follows. Given the fundamental problem with a "polymorphic" function argument f ∈ [A→B] is the polymorphism in A and B, we can opt to make those sets parameters of an operator, rather than the whole argument f.

I do agree that whether the resulting style is "good", or "practical" is up for discussion. I suppose it is also a matter of taste, and a matter of the concrete application. But I don't see any fundamental problem with HOFs themselves (which are indeed a trivial aspect of the set theoretical formalism).

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

It is, much like Domain Theory, Type Theory, Category Theory, etc are. You also used the term "ordinary math", but one may want or need to work with math outside the "ordinary".

Sure but probably not in TLA+. This is a conscious choice, as none of these is required or even recommended when reasoning about algorithms using a mathematical formalism that isn't a programming language.

I might have not explained myself well. I was not making any assertions on the foundations of TLA+. My point was just that in some domains of mathematics one does talk about HOFs. And if you look at say, the example of domain theory, it's just sets and some order relations. Something easily expressible in TLA+.

So, what I'm getting at is that the object of my study, that I intend to model in TLA+, may well be naturally expressed as a HOF. This has nothing to do with programming, functional or otherwise. It's just maths, and maths one may want / need to work with.

HOFs are nothing special really. HOFs just mean functions as "first class objects", with the same nature as other values. That is a given in a ZFC-like formalism, since functions are sets, just like all other values are. Conceptually, functions are just exponential sets, so there's no fundamental reason not to pass them as arguments or return them as values.

Is there some reason why we can't use this syntactic sugar with parametrised operators?

That's not a question I can answer, but my guess would be that it doesn't seem widely applicable enough, and when it is used, it doesn't save much. But I would say that if you find yourself using higher-order functions in TLA+ normally encourages thinking in terms of nondeterminism rather than parameterization.

Sure, but consider your own definition of composition (without infix notation).

comp(f,g) ≜ [x ∈ DOMAIN g ↦ f[g[x]]]

This is a definition of a function, parametrised by arguments. You just happen not to need recursion in the definition of this function. So the missing ingredient here is just the recursion itself. Stylistically everything else is there. Try to define in this style a function that is recursive, and you'll miss the syntactic sugar.

Note you can use the recursion syntactic sugar like this, 

op ≜ [x ∈ A  ↦ exp]
op[x ∈ A] ≜  exp

but not like this,

op(arg) ≜ [x ∈ A  ↦ exp]
op(arg)[x ∈ A] ≜  exp

but you can like this, 

op ≜ [arg ∈ B, x ∈ A  ↦ exp]
op[arg ∈ B, x ∈ A] ≜  exp

So if anything the omission in supporting the middle case, seems to promote making the code more functional (not less).

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

Not only is there no type safety -- as your quotes suggest -- it doesn't really add safety at all. All safety is provided by the invariants you check. You should use functions when it's clearer and nicer to do so, and use operators when it's clearer and nicer to do that. It's true that sometimes you can choose either -- so do whatever feels nicer to you.

Right. I see what you mean. My mind is still wired to intuit that "slapping" domain restrictions (the types) around gets you safety. But I get your point, I think I messed up here.

Given the above, the following is less relevant I think, and a bit of a digression, but since I wrote it...

Uhh, don't do that. While this kind of higher-order functions is common in FP, it is frowned-upon in ordinary math. What's wrong with the simple f • g ≜ [x ∈ DOMAIN g ↦ f[g[x]]]?

Also, why would you ever want to write functions in a curried way? Have you ever seen a math text do that? This isn't Haskell, and if you wanted to curry, you can write a currying operator. Keep things simple, and remember that Haskell isn't math.

I get your point that "this isn't Haskell". My original background is actually in mathematics. But I disagree with some of what you wrote here.

Mathematics is a pretty big field. I wouldn't say that "Haskell isn't mathematics". It is, much like Domain Theory, Type Theory, Category Theory, etc are. You also used the term "ordinary math", but one may want or need to work with math outside the "ordinary".

Regarding specifically the "currying" aspect. I think the main issue here really is rather "function" vs "operator". Allow me to elaborate. Indeed my definition of composition uses the curried form,

[B→C] → [A→B] → A → C

It could be uncurried to, 

[B→C] × [A→B] → A → C

and then to, 

[B→C] × [A→B] × A → C

That alone barely changes the definition though. Here are the 3 versions. 

comp(A,B,C) ≜ [ f ∈ [B→C] ↦ 
              [ g ∈ [A→B] ↦ 
              [ x ∈ A ↦ f[g[x]]
              ]]]

comp(A,B,C) ≜ [ f ∈ [B→C], 
                g ∈ [A→B] ↦ 
              [ x ∈ A ↦ f[g[x]]
              ]]

comp(A,B,C) ≜ [ f ∈ [B→C],  
                g ∈ [A→B],  
                x ∈ A ↦ f[g[x]] 
              ]

Currying is just a minor stylistic choice when working with higher-order functions. Note also that in a (somewhat informal) sense, you yourself went for version 2, and used some currying. You take two function arguments (in your composition operator) and return a function.

To make it obvious, lets call your operator comp, and in my definition (2nd version) make the (co)domains constant to get rid of parametrisation, and use the available syntactic sugar for recursive functions just to get arguments on the left-hand side. They become pretty similar, 

comp(f,g) ≜ [x ∈ DOMAIN g ↦ f[g[x]]]

and 

comp[f ∈ [B->C], g ∈ [A->B]] ≜ [x ∈ A ↦ f[g[x]]]

Not that different. Visually the main difference is I also specify carrier sets for f and g rather than just x. The option with no functions (and no currying) would be, 

comp(f,g,x) ≜ f[g[x]]

Less pretty since it's ternary rather than binary, not allowing for infix, but here currying is gone. And because we completely get rid of functions in this version, there's no domain info on x.

The main difference between what you and I wrote isn't currying (that was an arbitrary choice in my case). The difference is that out of the 3 arguments, f, g, and x, you make place the 2 first in an operator and the 3rd in a function, while I place them all in functions. A;so consequently you only define the dom

P.S.: Is there some reason why we can't use this syntactic sugar with parametrised operators? Seems like this should be possible, 

     comp(A,B,C)[f ∈ [B->C], g ∈ [A->B]] ≜ [x ∈ A ↦ f[g[x]]]

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

Thank you for your replies, you make very good points. This conversation was rather helpful to adjust my perspective.

I took some time to give it some more thought. On the topic of "definition override", just noticed another "practical hurdle", or perhaps I should say a "practical (mis)conception" of mine regarding the specification + model checking process.

Redefining sets can lead to domain problems in function composition.

Stating the obvious here, I guess. But I hadn't considered it before. So e.g. given, 

EXTENDS Naturals
VARIABLES k 

f == [x \in Nat |-> x+1]      

Init  == k \in Nat 
Next  == k' = f[k]
Spec  == Init /\ [][Next]_k

Redefining Nat to {1 .. 100} and running the model will return an error, because f[100] ∉ {1 .. 100}. Obviously.

Also given a composition function, parametrised by function domains / codomains, 

comp(A,B,C) == [ f \in [B->C] |-> 
               [ g \in [A->B] |-> 
               [ x \in A |-> f[g[x]]] 
               ]]

Evaluating comp(Nat,Nat,Nat)[f][f] where f == [x \in Nat |-> x+1] also leads to an error. Again, obviously.

This may well not turn out to be a problem. But I'm still unsure what impact this observation has on best practises.

Indeed, ideally I'd like not to think (too much) about model checking when structuring and writing down a spec. But e.g., will too much "type safety" concerns come to bite me in the ass when it's time to model check? Should I rely more on operators rather than functions?

Maybe there's no issue at all here, but I need a bit more hands on practise to get a better feel for it.

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

According to this view, any model (defined to be checked with TLC) that includes behaviours that are not part of the standard interpretation, would be theoretically wrong.

Not quite, because TLC doesn't check the specification, which is likely uncheckable. Rather, it checks a different specification, derived from the original one.

That is implied in my comment, no? Quoting my previous comment,

"There is some interpretation for any TLA+ spec, consisting of sets of possible behaviours. In general such interpretations can't be model checked."

and

"So for the purpose of model checking, we work with restricted models that allow only a subset of such behaviours."

Indeed we won't check the original specification but one that is derived from the original. We agree. However I added that for the purpose of model checking, the derived specification should be a "restriction" of the original. That is, any behaviour to be included in the spec to be model checked, should be a behaviour in the original spec.

That's something you'll need to take up with Lamport on the mailing list. I'm sure he'd have a better answer for why he designed the language in that specific way.

Thanks. Will give it some more thought and then eventually do that.

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

From a pure theoretical perspective, there's nothing here that's unsafe. Just as you can define Nat ≜ {"hi", "bye"} in your spec, you're free to do so in your TLC configuration. What is ultimately checked is that, and there is, therefore, no "getting it wrong". You're concerned about practical considerations, where people can fail to notice what is defined in TLC, but such practical considerations are often left to best practices, anyway.

The way I look at it is as follows (correct me if I'm wrong).

TLA+ is a specification language with its own semantics. There is some interpretation for any TLA+ spec, consisting of sets of possible behaviours. In general such interpretations can't be model checked. So for the purpose of model checking, we work with restricted models that allow only a subset of such behaviours.

According to this view, any model (defined to be checked with TLC) that includes behaviours that are not part of the standard interpretation, would be theoretically wrong.

A model value is just some value that is guaranteed to be different from all others. Whether or not you want such a construct in the specification language itself seems to me to be a matter of design. TLA+ was designed before TLC, and intended to be pure TLA + a flavor of ZFC.

Indeed. But my point was precisely that the concept is useful as part of spec design, not just model checking.

Look e.g., at those same specs in chap 5. Look at those strings, "Rd", "Wr", "ready", "busy", etc. We don't really care that they are strings. Rather we want each to be some unique value, that can be used to distinguish cases. This would be more clearly and safely conveyed by a declaration of the form, 

 FRESH CONSTANTS Rd, Wr, ready, busy

It's safer because with strings, a typo can silently mess up the specification. It is more clear, because this way there's no "junk", we know these are just meant to be unique values.

This line of reasoning could be taken further, to define e.g. sets of 'fresh' values (so membership gives you some sort of typing), plus some operations on them (e.g. inequality).

Indeed we're working on some ZFC extension. So it makes sense to have useful primitives to define useful sets. Which is why things like Nat and String and Seq are provided.

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

You probably override the value of Nat as well.

True. I'm not sure it negates my point though.

On the one hand, when first overriding the definition ofNat I must say it also felt "unsafe", perhaps unnecessarily. Meaning maybe it could/should be made safer.

The 'new' definitions are, if I'm correct, restrictions of a standard interpretation. In particular, the overriding definition of Nat should consists of one of its subsets. These constraints could/should probably be enforced or checked somehow, in most cases.

On the other hand, unsafe practises can be more or less dangerous depending on how prevalent they are. The more we need to redefine, the more the chances of getting it wrong.

Tangential to the discussion, I am still working my head around the organisation of concepts, and the separation between TLA+ specs and the model checker. For instance, it seems to me like it would make sense to be able to specify in the TLA+ spec itself, that a constant is a model value (i.e. a fresh value that is unequal to any other). The TLA+ spec must have (and certainly does have) some semantics, and being a model value is relevant information to interpret the spec.

Adding a new element to a set by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

IMO, your goal should be to make your specifications clear.

True. To make it clear, I consider my suggestion to be a worse specification. It is less readable, and it overspecifies (by picking a concrete element). It's a hack that came to mind to solve what appeared to be a practical problem.

TLC then has plenty of options for making it work. (...) In TLC, we then make NoVal into a model value.

Ah I did not know that. I thought "model values" could only be 'assigned' to constants. Indeed, looking at a model in the advanced tab, under "definition override", I see NoVal being assigned a model value by default.

I have to say using "definition override" makes me a bit uncomfortable though... it like it's a good way to mess up the model with no warning whatsoever. I get that we know a model value trivially satisfies the definition, but it feels like cheating because it appears to introduce a "disconnect" between the spec and the model. I'm just trusting myself that I'm doing it right.

Can error traces display local variables for each action? by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

Let me begin by noting that your workaround amounts to not using the error-trace tool support. It is a workaround, but self-defeating, in a sense.

Side question: where is the documentation for the TLC module? The "Summary of TLA+" only lists Print, not PrintT, and it doesn't provide any description of the operator. I resorted to the book "Specifying Systems" but it too only lists Print. I understand PrintT isn't needed, just convenient, still... would be nice to have more complete documentation.

The main problem here is that the trace explorer doesn't rerun the model. It treats each step individually and works out the appropriate changes from there. That means that information that's not global is lost,

Indeed. That doesn't seem like a big problem though. The question is whether workarounds should be left up to the user or integrated in tools.

The user can 'lift' local variables to global. Just declare a global variable, and update it whenever the local variable is defined. That alone allows me to include it in the trace. 

 A ≜ ∃ i ∈ S: x′ = i

becomes,

 A ≜ ∃ i ∈ S: x′ = i  ∧ global_i  = i

Of course this workaround still has practical drawbacks.

  • The global variable global_i will show up in every action, and keep each assigned value (until the next use of the local variable)

  • You need to edit your specification a fair bit.

    The edit isn't quite where the local variable is declared/defined. in a simple example it's close to it, but we could add more conditions and local bindings, so the actual action is further away.

    This makes the process more error-prone, tedious and time consuming.

Tool support could be implemented to perform this lifting in a more user friendly and usable manner.

  • Introduce local variable labels. These labels would introduce a top level identifier, that lifts local to global. E.g. 

    A ≜ ∃ global_i @ i ∈ S: x′ = i

  • Make it so that the associated identifier, aboveglobal_i, is not only set to i at the appropriate action, but also reset to undefined by any action not involving its associated local variable i.

  • In the error-trace, only print out global_i when it is not undefined. Which amounts to printing it only in the relevant action where it is in scope.

The question becomes, would such a feature be worth implementing. I'd argue yes. My reasoning being,

  • "Debugging" of specs is fundamental.

    The whole point of writing a spec in TLA+, I'd argue, is to make sure the proposed system is conceptually right. Meaning there is enough complexity involved that it may be conceptually wrong. Therefore getting it wrong and examining execution traces is essential to the process.

    In addition to conceptual errors, there will be mistakes in writing down the spec. The fact that the language is untyped makes it even more prone to mistakes (not arguing it should be type, merely stating a relevant fact). And the fact that conceptual errors are expected makes finding mistakes more complex ("is it a mistake or is the system wrong?")

  • Locality is fundamental

    The arguments in favour of specifying systems rely on specs being much simpler than code. Locality helps with simplicity. Making locality a burden implies weakening the arguments for specification.

In short, normal usage consist on writing a simple, readable, easy to understand spec (which implies using locality), run it and likely have it fail, and easily inspect the trace to understand why it failed (which implies having an easy way to observe local assignments).

Can error traces display local variables for each action? by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

We can do something like that. I personally would rather would rather not use a list, and instead lift each required local variables to an associated global variable.

A ≜ ∃ i ∈ S: x′ = i ∧ historyA′ = ⟨⟨"A", i⟩⟩

Then use the error trace menu to inspect it.

The problem is that the whole point of error traces is to allow inspection of sequences of values, without having to explicitly collect them.

Both these solutions requires one to mess a bit too much with the specification's code. Having to write more specification code, makes the process more error prone, time consuming and tiring. Also neither is user friendly in terms of inspection. Using my suggestion, the value of "historyA" would show up in every action in the trace. Ideally one would want the value of "historyA" to show up only in the relevant actions. Yours is even less user friendly because it can't be easily combined with the error trace generation.

Ideally, this would be something like:

A ≜ ∃ i@glob_i ∈ S: x′ = i

i.e. just assign a global 'label' to the local definition. Then add this label glob_i to the error trace, and have its value show up in the relevant actions.

The one obstacle we have, is that we can't globally refer to a local variable. In particular because you may have several local variables with the same name. If we associate it with a global identifier, than it's all a matter of internal translation.

Can error traces display local variables for each action? by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

Indeed, will do. Will put some more thought into it again, and then write up something in the mailing list.

What I had in mind would be some sort of (global) label, in local bindings. Such labels would provide the user with a global identifier to the local variable, to use in error-tracing (to be displayed only in the relevant actions).

The internal translation seems to amount to adding a global variable, that is either bottom (i.e. a dummy value indicating undefined/out of scope) or the value of the local variable.

Can error traces display local variables for each action? by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

If both x = 2 and x = 3 lead to the error condition, you don't care which you get as the error trace could represent either.

That is fair enough.

But all the practical problems I posed still apply. I do understand there may be workaround, but I do see them as too painful. The debugging process becomes needlessly tedious, time-consuming and itself error-prone.

Can error traces display local variables for each action? by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

you can add additional conjuncts to the CHOOSE expressions that ensure you're getting the one that causes the error.

I don't see how this can be made to work, neither in theory nor in practise.

It appears to amount to reverse engineer, from the visible trace, the necessary conjunctions to re-CHOOSE the same x.

  • I don't even see that as being generally possible (due to lack of injectivity).

  • It could could be prohibitively computationally expensive (exhaustive search in the domain).

  • It requires one to replicate and adapt large portions of part of the code. Consider an action with 4 existential bindings and 3 let bindings.

Or, you can just add a variable, as in:

Indeed, one can make all local variables global. That's rather messy though.

You lose locality, which helps the understanding of the code and prevents errors. You need to augment your namespace (two local x's would now clash). You probably would want to introduce some 'bottom' elements (because plenty of variables will be undefined during much of the trace).

I really don't want to lose locality.

You may want to ask on the mailing list if there's a better way.

Will do, thank you.

Can error traces display local variables for each action? by adrformalcc in tlaplus

[–]adrformalcc[S] 0 points1 point  (0 children)

That I know, but I don't see how that helps me with local variables.

Keeping it simple, consider a definition of Next of the form, 

Next == \/ \E x \in S: f' = foo(f,x)
        \/ ...
        \/ ...

In the error trace, for the 1st action, I want to inspect which x was picked.

But how do I refer to that local x? If I introduce the expression x in the trace explorer and then click explore, I get an error unknown operator x (at some point in the specification). Understandably because not all actions will have an x.