|
> Do you mean you can't pass an operator to a function Right. Functions are objects in the theory, and must have a domain which is a set. Operators are outside the theory, and aren't in any sets. You also can't return an operator as a result of an operator. A function can, of course, return a function, but functions can't be polymorphic within a single specification. So they must have a particular (though perhaps unspecified) set as their domain. Why? Because there is no such thing as polymorphic functions in math. Polymorphism is a feature of a certain language or "calculus", and TLA+ is about algorithms, not about a specific linguistic representation of them. "Polymorphism" of the kind I've shown does make sense, because you determine the level of the specification, and you can say that you want to reason about the use of a function (or a computation) without assuming anything more specific other than your explicit assumptions about a certain set. But that is not to say that you can’t have an operator that “creates” functions generically. E.g.: Foo(a) ≜ [x ∈ a × a ↦ x[1]] /or/ Foo(a) ≜ LET f[x ∈ a × a] ≜ x[1] IN f
Which you can then use like so: Foo(Nat)[1, 2]. Foo must be an operator because its argument `a` ranges over all sets, so it's not a proper domain (Russel, etc.)> or make it the argument of a computation Ah, that actually you can do, and it's quite common as it's very useful. A constant can be an operator (a variable can't because a variable is state, and state must be an object in the theory). For example, it's useful for taking a relation as input (although a relation can also be defined as a set of pairs, so it’s an object in the theory). If in the polymorphic example you want to say that the set `a` is partially ordered (because you're specifying a sorting algorithm), you can write[1]: CONSTANTS a, _ ⊑ _
ASSUME ∀x, y, z ∈ a :
∧ x ⊑ x
∧ x ⊑ y ∧ y ⊑ x => x = y
∧ x ⊑ y ∧ y ⊑ z => x ⊑ z
All of this, BTW, is actually the "+" in TLA+ (which is a bit technical, and trips me up occasionally), and not where the core concepts lie, which is the TLA part. Lamport would say you’re focusing on the boring algebraic stuff, rather than the interesting algorithmic stuff… I guess you could come up with another TLA language, with a different "+", but the choice of this particular "+" (i.e, set theory) was made after experimentation and work with engineers back in the '90s (Lamport says that early versions were typed). There is actually a type inferencer for TLA+, which is used when proofs are passed to the Isabelle backend (or intended to be used, I don't know; the proof system is under constant development at INRIA). So you get rich mathematical reasoning using simple math — no monads or dependent types (nor any types) necessary. Those things can be useful (for automatic code extraction, maybe, or for deep mathematical theories of languages — not algorithms), but for mathematically reasoning about programs, this is really all you need. And it works well, in the industry, for programs as small as a sorting routine or as large as a complex distributed database.[1]: The aligned conjunctions are a syntactic convenience to avoid parentheses. |