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

Re: Recursive data structures

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


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:


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.