Consider the following function on binary trees, which is supposed to tell whether a given int
is a member of a binary tree t
:
type tree = Leaf | Node of int * tree * tree;;
let rec tmember (t:tree) (x:int) : bool =
match t with
Leaf -> false
| Node (j,left,right) -> j = x || tmember left x || tmember right x
;;
If one wants to prove that this function is correct, one would need to define first what tree membership actually means, but then I can find no formal way of doing this except for saying that x
is a member of t
if and only if it is either equal to the root of t
, or it is a member of the left or right subtree of t
. This is essentially saying that x
is a member of t
if and only if tmember t x
outputs true
.
What am I missing here?
tmember
. However, you can still prove things about it that you would expect of a membership relation, such as empty trees have no elements and if you insert an element into a tree thentmember
gives true. $\endgroup$tmember
function? $\endgroup$