How to talk about any objects mathematically? (In this case binary trees)

Question

For context I was doing the following exercise in Isabelle theorem prover tutorial:

Let datatype 'a tree = Tip "'a tree" 'a "'a tree"

1. Define a function set :: 'a tree => 'a set which transforms a tree into a set
2. Define a function ord :: 'a tree => bool which checks if a tree is ordered

Now when I was doing the 2nd task, I wanted to think about it mathematically instead of just as a function in isabelle. Btw in this case a tree is ordered if for any node $x$, all the nodes in the left subtree are less than $x$ and all the nodes in the right subtree are greater than $x$. For example this tree is ordered:

      10
    /   \
   5     15
  / \    /  \
 2   7  12  18

If we look at that tree, we can flatten the tree like this:
2 5 7 10 12 15 18

I don't know what that sequence or list is called but in that sequence for any node $x$, all the elements to the left are nodes in the left subtree of $x$. For example if we take 10 in that sequence, then 2, 5 and 7 are all elements of the left subtree of the node 10.

If we think about a binary tree by taking that type of sequence above, call it $a_0, a_1, ... , a_n$ then the binary tree is ordered if $a_i < a_{i+1}$ for all $i$ (i think) The best way i can describe the tree is that we let $a_0$ be the left most node in the entire tree and then $a_1$ is the parent of that, then $a_2$ is either the right child node of the parent, or it's the parent of $a_1$ ... (this is not a very good description)

Thinking about the problem like that is way more fun than just trying to implement the function ord :: 'a tree => bool in a certain programming language, but the issue here is that this explanation above is definitely not a valid explanation mathematically. How would the sequence $a_0,a_1, ... , a_n$ actually be defined? Can I define it myself or does it have to be like standard or something?

If I want to talk about any objects kind of mathematically like this, how can I do it? It's ok to talk about this problem with the sequence $a_0,a_1,...,a_n$ if I can actually define it properly right?

Answer 1

To define such flatten function $f$ from a binary tree to a sequence, one way is to define

• $f$ of empty tree be the empty sequence $()$, and
• $f$ of a tree with root value $x$, left subtree $L$ and right subtree $R$ be (recursively) $$f(L) \oplus (x) \oplus f(R),$$ where $\oplus$ denotes sequence concatenation.

This is similar to how one may define such function in a program.