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}

Leslie

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:

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