Re: [tlaplus] Recursive data structures

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

On Thursday, August 31, 2017 at 9:50:16 AM UTC+3, Stephan Merz wrote:

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

On 30 Aug 2017, at 23:09, Hillel Wayne <hwa...@xxxxxxxxx> wrote:

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...@googlegroups.com.
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.