implement semantics using agda functions

[cyrus-]

and prove them sound and complete*

• where completeness requires us to first figure out how we ultimately want to talk about determinism, i.e. #16

I'm not sure if we'll run into any problems with the termination checker...?

It might also be useful to see what the Agda Haskell backend does with such a function, since it should look more or less like a Haskell function. don't try too hard to get extraction to work, but if its simple, it'd be cool to do.

[ivoysey]

migrating this to the issue tracker repo.