程序代写代做代考 compiler html Haskell 12/08/2020 Exercise (Week 8)

12/08/2020 Exercise (Week 8)
Exercise (Week 8)
DUE: Wed 29 July, 2020 15:00 CSE
Stack
Download the exercise tarball and extract it to a directory on your local machine. This tarball contains a le, called Ex06.hs , wherein you will do all of your programming.
To test your code, run the following shell commands to open a GHCi session:
$ stack repl
Configuring GHCi with the following packages: Ex06
Using main module: 1. Package ‘Ex06’ component exe:Ex06 …
GHCi, version 8.2.2: http://www.haskell.org/ghc/ 😕 for help
[1 of 1] Compiling Ex06 (Ex06.hs, interpreted)
Ok, one module loaded.
*Ex06> solutions e3
…
Note that you will only need to submit Ex06.hs , so only make changes to that le.
Logical formulas (often called constraints) ranging over nite domains (i.e., where variables are drawn from sets with a nite number of elements) are useful in a wide array of application areas ranging from solving planning problems, over compiler optimisations, to code verication. Given such formulas, we are usually interested in either whether there exists a solution (i.e. instantiation of all variables) that satisfy the logical formula or in the solutions themselves. You will have to perform the following tasks in this exercise:
● Write an evaluator for (unquantied) formula terms, using a GADT representation,
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/exercise.html
1/4

data Term t where
Con :: t -> Term t — Constant values
— Logical operators
And :: Term Bool -> Term Bool -> Term Bool Or :: Term Bool -> Term Bool -> Term Bool
— Comparison operators
Smaller :: Term Int -> Term Int -> Term Bool
— Arithmetic operators
Plus :: Term Int -> Term Int -> Term Int
Plus (Con 2)
Con True
Term Bool
(Con 10)
Term Int
data Formula ts where
Body :: Term Bool -> Formula ()
Exists :: Show a
=> [a] -> (Term a -> Formula as) -> Formula (a, as)
ex3
Exists [False, True] $ \p ->
Exists [0..2] $ \n ->
Body $ p `Or` (Con 0 `Smaller` n)
12/08/2020
● ●
Exercise (Week 8)
check for the satisability of logical formulas, and compute the solution set of logical formulas.
We will do that for a very simple logic to keep it manageable, namely formulae of the form:
where is a term without any quantiers and the sets are all nite. 1
Our language of quantier-free terms is indexed by the type of the term: 1
For example, the term is of type , and the term is of type .
Our language of formulae (including quantiers) is indexed by the types of each quantied variable:
For example, the following formula ( in the code):
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/exercise.html
2/4
nS … 1S φ φ.nS∈nx∃… .2S∈2x∃.1S∈1x∃

12/08/2020 Exercise (Week 8)
Has the type to reect the types of the two quantied variables.
Evaluating Terms (2 marks)
Write a function:
That recursively evaluates the term to its result.
Satisability check (3 marks)
Secondly, implement a function
that determines whether a given formula is satisable – i.e. whether there is an assignment of values to all existentially quantied variables (those with the Exists constructor), such that the body of the formula evaluates to True . Given the examples provided in the code, we expect:
eval :: Term t -> t
satisfiable :: Formula ts -> Bool
*Ex06> satisfiable ex1
True
*Ex06> satisfiable ex2
True
*Ex06> satisfiable ex3
True
Enumerating Solutions (4 marks)
Finally, implement
which computes a list of all the solutions for a Formula . Each individual solution is of the same type as the type index of the formula with one value for each existentially quantied variable. Again, considering the examples from Formula.hs , we expect:
solutions :: Formula ts -> [ts]
Formula (Bool, (Int, ()))
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/exercise.html
3/4

12/08/2020 Exercise (Week 8)
What would be the result for a formula that is not satisable?
Note: You can use the list monad or list comprehensions here to make solutions a
very short denition.
Submission instructions
on a CSE terminal, or by using the give web interface. Your le must be named Ex06.hs (case-sensitive!). A dry-run test will partially autotest your solution at
submission time. To get full marks, you will need to perform further testing yourself.
Footnotes:
1
1 Note that there is also a Name constructor given in the code, however this
constructor is only used for pretty printing and is not relevant to any of the functions you have to implement.
$ give cs3141 Ex06 Ex06.hs
*Ex06> solutions ex1
[()]
*Ex06> solutions ex2
[(1,()),(2,()),(3,()),(4,()),(5,()),(6,()),(7,()),(8,()),(9,()),(10,())]
*Ex06> solutions ex3
[(False,(1,())),(False,(2,())),(True,(0,())),(True,(1,())),(True,(2,()))]
www.cse.unsw.edu.au/~cs3141/20T2/Week 08/exercise.html
4/4