How can I translate a Haskell code segment to a mathematical representation?

Question

I am trying to translate some Haskell code to a mathematical notation. Below is a Haskell program that represents a stack of physical blocks.

-- set of blocks
data Block = B1  | B2 | B3  | B4 | B5 | B6 | B7 | B8   deriving (Eq,Show) 
-- MoveOnto(bl,b2,t) is read as b2 is moved into and onto bl on table t.
data Stack = EmptyTable  |  MoveOnto Block Block Stack deriving Show 
isOn :: Block -> Block -> Stack -> Bool
isOn b1 b2 (MoveOnto b3 b4 s) |  ((b1 == b3) && (b4 == b2)) || 
                                  (isOn b1 b3 s)  || 
                                  (isOn b4 b2 s) =  True                        
isOn _ _ _  = False                             

testTransitivityTrue = 
    isOn B1 B4 (MoveOnto B1 B2 (MoveOnto B2 B3 (MoveOnto B3 B4 EmptyTable)))
testTransitivityFalse = 
      isOn B3 B1 (MoveOnto B1 B2 (MoveOnto B2 B3 EmptyTable)) 

Blocks can only be placed on a table or another block using constructors EmptyTable and MoveOnto. The Boolean function isOn is a decision procedure for deciding whether a given block is on top of another.

Here is my attempt at a mathematical representation: $$Blocks = \{ B_1 \ldots B_{10} \}$$ $$Stack = \{ EmptyTable \} \cup $$ $$\{ MoveOnto(B_1,B_2,EmptyTable), MoveOnto(B_2,B_1,EmptyTable),\ldots \} \cup$$ $$\{ MoveOnto(B_3,B_2,(MoveOnto(B_2,B_1,EmptyTable))), \ldots \}$$ The two sets above, $Blocks$ and $Stack$, consist of all possible constructed terms for the block world algebra. I did not include the detailed subscripts. The following is my attempt at representing the Boolean Function isOn. $$ isOn(b_1,b_2,MoveOnto(b_3,b_4,s)) = \begin{cases} true, & \text{if } (b_1 = b_3) \land (b_4 = b_2) \\ true, & \text{if } isOn(b_1,b_3,s) \\ true, & \text{if } isOn(b_4,b_2,s) \\ false, & \text{if } isOn(b_1,b_2,EmptyTable) \end{cases}\\ $$

I don't think that I can use Haskell's otherwise clause for the false case. I use wildcard or don't care pattern instead of explicit variables. I believe that this due to pattern matching, where EmptyTable cannot match MoveOnto(b3,b4,s). I am not sure of how this could be represented mathematically. Can otherwise be used in the the math? Both the terms $EmptyTable$ and $MoveOnto(b_3,b_4,s)$ are in the set $Stack$.

Answer 1

Many people use "otherwise" in case notation, see for example here, and it is a bit cleaner:

$$ \operatorname{isOn}(b_1,b_2,\mathtt{MoveOnto}(b_3,b_4,s)) = \begin{cases} \mathtt{true} & \text{if } (b_1 = b_3) \land (b_4 = b_2) \\ \mathtt{true} & \text{if } \operatorname{isOn}(b_1,b_3,s) \\ \mathtt{true} & \text{if } \operatorname{isOn}(b_4,b_2,s) \\ \mathtt{false} & \text{otherwise} \end{cases}\\ $$

While not necessary, it is useful to keep the variables, operators and constants distinct. There is a difference between $$\sin\alpha$$ and $$sin \alpha,$$ and for the same reason I've used \mathtt for MoveOnto constructor and constants true and false; there are also symbols $\top$ and $\bot$, but I find these less readable.

Regarding the sets, you might want to prefer \begin{align} B &= \{\mathtt{B}_1, \ldots, \mathtt{B}_{10}\}, \\ S_0 &= \{\mathtt{EmptyStack}\}, \\ S_k &= \{\mathtt{MoveOnto}(b_1, b_2, s) \mid b_1, b_2 \in B, s \in S_{k-1}\}, \\ S &= \bigcup_{k \in \mathbb{N}} S_k. \\ \end{align}

I hope this helps $\ddot\smile$