Homework 12: Stack Language
This is an exercise to practice (small-step) operational semantics. Consider the abstract syntax for the operations of a small stack language.
data Op = Push Nat | Pop | Add
A stack is represented by a list of natural numbers.
Stack : Type
Stack = List Nat
(a) Define the small-step operational semantics for the operations as a ternary relationship that contains triples of the following form.
(old stack,operation,new stack)
This relationship should be implemented as an Idris data type of the following type.
data Step : Stack -> Op -> Stack -> Type where
…
(b) With Step we can describe the effect of individual operations on a stack, but we cannot express the meaning of stack programs. A stack program is given by a list of operations.
Ops : Type
Ops = List Op
Define the semantics of stack programs as a ternary relationship, implemented as an Idris data type of the following type.
data Steps : Stack -> Ops -> Stack -> Type where
…
Note: You probably need two constructors, one for an empty list of operations and one for a non-empty list, and the argument type of one of these constructors has to refer to the type Step defined in part (a).
(c) Determine the semantics of the following stack program, express it as an Idris type using Steps, and prove the statement.
[Push 3,Push 5,Add]