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

RE: [tlaplus] Recursive data structures

At first glance, the definition you seem to want could be written like this:


  Node ==  CHOOSE Node : Node = [key : Key,

                                 value : Value,

                                 leftChild : Node,

                                 rightChild : Node]


This is a legal TLA+ definition (though not one that TLC can handle because of the unbounded CHOOSE).  However, it doesn’t specify a set Node that you want because there are multiple choices of a set Node satisfying the body of the CHOOSE.  I can think of two such sets: a set of infinite-depth binary trees, and the empty set. 


Actually, the key component in what you wrote confuses me.  If each node has a unique key, then you can define an arbitrary graph of nodes with


Node ==

    [key : Key,
     value : Value,
     leftChild : Key,
     rightChild : Key]


Do you want to define the set of finite binary trees where each node has a value, like this?


          . 14

         / \

        /   \

       . 7   . 24

      / \   

     /   \

    . 6   . 11


In that case, you can recursively define


 Tree == LET TreeOfDepthAtMost[n \in Nat] ==

                 IF n = 0 THEN [value : Value]

                          ELSE [value : Value,

                                leftChild : TreeOfDepthAtMost[n-1],

                                rightChild : TreeOfDepthAtMost[n-1]]

                                \cup  TreeOfDepthAtMost[n-1]


          IN  UNION {TreeOfDepthAtMost[n] : n \in Nat}




From: tla...@xxxxxxxxxxxxxxxx [mailto:tla...@xxxxxxxxxxxxxxxx] On Behalf Of Andrew Helwer
Sent: Tuesday, August 29, 2017 1:46 PM
To: tlaplus <tl...@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Recursive data structures


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:


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+unsu...@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.