CS代考计算机代写 Homework 11: Move Language

Homework 11: Move Language

Consider the abstract syntax of the following language for describing movements in the 2D plane. Up moves one unit up, Rgt moves one unit to the right, Seq combines two moves, and Rev reverses the direction of a move.
data Move = Up | Rgt | Seq Move Move | Rev Move
The meaning of a Move program is given by a 2D vector, which is given by two integers.
Vec : Type
Vec = (Int,Int)
(Don’t confuse this type with the Vect n a type for vectors of specific lengths.)


(a) Define a denotational semantics of the Move language as a function sem with the following type.
sem : Move -> Vec
…
Note 1: For the semantics of Seq you may want to use an auxiliary function vadd for adding two vector values.
vadd : Vec -> Vec -> Vec
vadd …
Note 2: In the definition for Rev you should use a let definition (and not a where block).


(b) Define the big-step operational semantics for Move as a binary relation, which relates moves to vector values. This relationship should be defined as an Idris data type.
data Final : Move -> Vec -> Type where
…

(c) Determine the semantics of the following move, express it as a type using Final, and prove it.
(Up `Seq` Up) `Seq` Rgt