This does not really solve the problem, just like the definition using CHOOSE that Leslie gave in his answer: TLA+ doesn't commit to choosing a least or greatest (or any other) fixed point, and as Leslie pointed out, the definition has two fixed points, namely the empty set (least fixed point) and the infinite tree (greatest fixed point). So the meaning of your RECURSIVE definition is not uniquely specified, whatever TLC may give you (if it is at all able to evaluate it, which I haven't tried). I presume Andrew meant to define finite trees and forgot including a terminal case corresponding to null pointers for the children.
The definition suggested by Leslie essentially computes the least fixed point of that structure by making the depth explicit, and it can be approximated by TLC (by overriding Nat to be a suitable finite interval).
Stephan
TLA+2 (standard with toolbox) adds a RECURSIVE operator, so you can do
RECURSIVE Node
Node == [ key : Key, value : Value, leftChild : Node, rightChild : Node ]
On Tuesday, 29 August 2017 15:46:02 UTC-5, Andrew Helwer wrote: What is the canonical way to represent recursive data structures in TLA+? Consider the example of a binary tree; at first pass, we try to represent it as follows: CONSTANTS Key, Value
Node ==
[key : Key,
value : Value,
leftChild : Node,
rightChild : Node]
However, the syntactic analyzer gives the parser error "Unknown operator: Node" since recursive definitions are not supported here. We can borrow from Specifying Systems section 11.1.2 and define a generalized graph in terms of sets of nodes & edges with restrictions, but I'm interested in whether there are other ways to accomplish this goal.
--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|