Recursive data structures

[Andrew Helwer]

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.

[Leslie Lamport]

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}

 

Leslie

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Hillel Wayne]

TLA+2 (standard with toolbox) adds a RECURSIVE operator, so you can do

RECURSIVE Node

Node == [ 

  key : Key,

  value : Value,

  leftChild : Node,

  rightChild : Node

]

[Stephan Merz]

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

[Ron Pressler]

But if instead we define:

    NULL == "-"

and then,

    

    RECURSIVE Node

    Node == {NULL} \cup [value : Value, left : Node, right : Node]

(or Node == CHOOSE Node : Node = {NULL} \cup [...])

then aren't there just two fixpoints -- one with all finite trees and one with all finite and infinite trees? It's possible (depending on the spec) that we could live with either.

Also, at the danger of stating the obvious, if this is just needed for TLC and the goal is just to use trees in another algorithm rather than explore the properties of algorithms focused on trees, the most practical solution is just not to define the set Node at all...

Ron