-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
10 changed files
with
838 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,176 @@ | ||
# $\lambda$-Calculus Evaluator | ||
|
||
|
||
This homework assignment aims to implement an evaluator of $\lambda$-expressions in Haskell, | ||
reducing a given $\lambda$-expression into its normal form following the normal order evaluation | ||
strategy. As a side effect, this homework assignment will also help you consolidate your knowledge | ||
of $\lambda$-calculus. The $\lambda$-expressions will be represented as instances of a suitably | ||
defined Haskell data type. So you will practice how to work with such types, in particular how to | ||
make it an instance of the Show class and how to use pattern matching with them. | ||
|
||
The interpreter should be implemented as a Haskell module called `Hw3`. Note the capital `H`. The | ||
module names in Haskell have to start with capital letters. As the file containing the module code | ||
must be of the same name as the module name, **all your code is required to be in a single file called | ||
`Hw3.hs`**. Your file `Hw3.hs` has to start with the following lines: | ||
|
||
```haskell | ||
module Hw3 where | ||
|
||
type Symbol = String | ||
data Expr = Var Symbol | ||
| App Expr Expr | ||
| Lambda Symbol Expr deriving Eq | ||
``` | ||
The first line defines a module of the name `Hw3`. The names of variables in $\lambda$-terms are | ||
represented by instances of `String`. | ||
The second line just introduces a new name `Symbol` | ||
for the type `String` to distinguish visually when we deal with the variable names. The last line | ||
defines the data type representing $\lambda$-expressions. There are three data constructors: one for | ||
a variable, one for an application and one for $\lambda$-abstraction. The clause `deriving Eq` | ||
makes the data type instance of the `Eq` class so that it is possible to check whether two $\lambda$-expressions | ||
are equal or not. | ||
|
||
## Evaluator specification | ||
|
||
First, make the data type `Expr` | ||
an instance of the `Show` | ||
class so that `ghci` | ||
can display $\lambda$-expressions. So you need to define the `show` function converting | ||
$\lambda$-expressions into a string. Once you type into the `ghci` prompt the following | ||
expressions, it should behave as follows: | ||
```haskell | ||
λ> Var "x" | ||
x | ||
|
||
λ> App (Var "x") (Var "y") | ||
(x y) | ||
|
||
λ> Lambda "x" (Var "x") | ||
(\x.x) | ||
|
||
λ> App (Lambda "x" (Var "x")) (Var "y") | ||
((\x.x) y) | ||
|
||
λ> Lambda "s" (Lambda "z" (App (Var "s") (App (Var "s") (Var "z")))) | ||
(\s.(\z.(s (s z)))) | ||
``` | ||
So the symbol $\lambda$ is displayed as `\`. Variables are displays as their names. Applications | ||
are displayed as `(e1 e2)` | ||
with a space separating expressions `e1,e2` | ||
and $\lambda$-abstractions as `(\x.e)`. | ||
|
||
As a next step, your task is to implement a function | ||
`eval :: Expr -> Expr`. | ||
This function for a given input $\lambda$-expression returns its normal form if it exists. | ||
Moreover, it has to follow the normal order evaluation strategy. So to make a single step $\beta$-reduction, | ||
you have to identify the leftmost outermost redex and reduce it. Then you repeat this process until there | ||
is no redex. | ||
|
||
To reduce a redex, you have to implement the substitution mechanism allowing you to substitute a | ||
$\lambda$-expression for all the free occurrences of a variable in another $\lambda$-expression. | ||
This mechanism has to deal with name conflicts, as you know from the lecture on $\lambda$-calculus. | ||
One possibility how to safely do that is the following recursive definition: | ||
$$ | ||
\begin{align*} | ||
x[x:=e] &= e\\ | ||
y[x:=e] &= y \quad\text{if $y\neq x$}\\ | ||
(e_1\,e_2)[x:=e] &= (e_1[x:=e]\,e_2[x:=e])\\ | ||
(\lambda x.e')[x:=e] &= (\lambda x.e')\\ | ||
(\lambda y.e')[x:=e] &= (\lambda y.e'[x:=e]) \quad\text{if $y\neq x$ and $y$ is not free in $e$}\\ | ||
(\lambda y.e')[x:=e] &= (\lambda z.e'[y:=z][x:=e]) \quad\text{if $y\neq x$ and $y$ is free in $e$; $z$ is a fresh variable} | ||
\end{align*} | ||
$$ | ||
The last case deals with the name conflicts, i.e., it uses $\alpha$-conversion. | ||
As $y$ is free in $e$ in this case, it could become bound after the substitution in $e'$. | ||
Thus we rename $y$ in $\lambda y.e'$ to a new fresh variable $z$, i.e., we compute $e'[y:=z]$ and | ||
then replace the variable in the $\lambda$-abstraction to $\lambda z.e'[y:=z]$. | ||
Then we can continue and recursively substitute $e$ for $x$ in $e'[y:=z]$. | ||
So follow the above recursive definition in your code. | ||
|
||
Your code has to generate fresh symbols when needed. The fresh symbols can be denoted, e.g., | ||
`"a0","a1","a2",...`. | ||
To generate a fresh symbol, it suffices to increment the number of the last used symbol. | ||
This number is a state of your computation. As Haskell is a purely functional language, you cannot have a state | ||
and update it when necessary. Instead, you need to include the index into signatures of your functions | ||
similarly, as we did in the exercise from Lab 9 where we implemented a function indexing nodes of a binary tree. | ||
|
||
## Test cases | ||
|
||
Below you find several public test cases. If the $\lambda$-expression is already in its normal form, the `eval` | ||
function just returns its input. | ||
```haskell | ||
λ> eval (App (Var "x") (Var "y")) | ||
(x y) | ||
λ> eval (Lambda "x" (Var "x")) | ||
(\x.x) | ||
``` | ||
|
||
If it is reducible, it returns its normal form. For instance $(\lambda x.x)y$ is reduced to $y$: | ||
```haskell | ||
λ> eval (App (Lambda "x" (Var "x")) (Var "y")) | ||
y | ||
``` | ||
|
||
Consider the expression $(\lambda x.(\lambda y.(x\,y))y$. The reduction | ||
gives $(\lambda y.(x\,y))[x:=y]$. By the definition of substitution, we have to rename $y$ to $a0$ and then | ||
substitute $y$ for the free occurrences of $x$, i.e., | ||
$$ | ||
\begin{align*} | ||
(\lambda y.(x\,y))[x:=y] &= (\lambda a0.(x\,y)[y:=a0][x:=y])\\ | ||
&= (\lambda a0.(x\,a0)[x:=y])\\ | ||
&= (\lambda a0.(y\,a0)) | ||
\end{align*} | ||
$$ | ||
```haskell | ||
λ> eval (App (Lambda "x" (Lambda "y" (App (Var "x") (Var "y")))) (Var "y")) | ||
(\a0.(y a0)) | ||
``` | ||
|
||
Consider the $\lambda$-expression $(\lambda x.(\lambda y.y))y$. The reduction leads to $(\lambda y.y)[x:=y]$. | ||
As $y$ is free, we introduce by the definition a fresh variable $a0$ instead of $y$ obtaining | ||
$\lambda a0.y[y:=a0] = \lambda a0.a0$. Then we compute $\lambda a0.a0[x:=y] = \lambda a0.a0$. | ||
```haskell | ||
λ> eval (App (Lambda "x" (Lambda "y" (Var "y"))) (Var "y")) | ||
(\a0.a0) | ||
``` | ||
|
||
Consider the $\lambda$-expression $(\lambda x.(\lambda y.(\lambda z.((xy)z))))(y\,z)$. | ||
As $y$ and $z$ are free in $(y\,z)$ we have to rename them in $\lambda x.(\lambda y.(\lambda z.((xy)z)))$ | ||
obtaining $\lambda a0.(\lambda a1.(((y\,z)\,a0)\,a1))$. | ||
```haskell | ||
ex = App (Lambda "x" | ||
(Lambda "y" | ||
(Lambda "z" (App (App (Var "x") (Var "y")) (Var "z"))))) | ||
(App (Var "y") (Var "z")) | ||
|
||
λ> eval ex | ||
(\a0.(\a1.(((y z) a0) a1))) | ||
``` | ||
|
||
To write more complex test cases, you can define subexpressions and then compose more complex ones. | ||
For instance, to test that $S1$ reduces to $2$: | ||
```haskell | ||
one = Lambda "s" (Lambda "z" (App (Var "s") (Var "z"))) | ||
suc = Lambda "w" | ||
(Lambda "y" | ||
(Lambda "x" | ||
(App (Var "y") | ||
(App (App (Var "w") (Var "y")) | ||
(Var "x"))))) | ||
|
||
λ> eval (App suc one) | ||
(\y.(\x.(y (y x)))) | ||
``` | ||
|
||
One more test case using the definition $one = \lambda s.(\lambda z.(s\,z))$. Consider the $\lambda$-expression | ||
|
||
$$(\lambda z.one)(s\,z) = (\lambda z.(\lambda s.(\lambda z.(s\,z))))(s\, z).$$ | ||
|
||
It reduces to $\lambda a0.(\lambda z.(a0\,z))$. As $s$ is free in $(s\, z)$, the bound occurrence of $s$ in $one$ is renamed. | ||
But $z$ is not renamed because | ||
by the defition of substitution we have | ||
$\lambda z.(a0\, z)[z:=(s\,z)] = \lambda z.(a0\, z)$. | ||
```haskell | ||
λ> eval (App (Lambda "z" one) (App (Var "s") (Var "z"))) | ||
(\a0.(\z.(a0 z))) | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,158 @@ | ||
# Lab 8: Haskell basics | ||
|
||
The aim of the lab is to practice function definitions using pattern matching and guarded equations together with the list comprehension. | ||
|
||
## Exercise 1 | ||
Write a function `separate :: [Int] -> ([Int], [Int])` taking a list and returning a pair of lists. The first | ||
containing elements on indexes 0,2,4,... and the second on the indexes 1,3,5,... E.g. | ||
```haskell | ||
separate [1,2,3,4,5] => ([1,3,5], [2,4]) | ||
``` | ||
|
||
::: tip Hint | ||
Use pattern matching `x:y:xs` and recursion. | ||
::: | ||
|
||
|
||
::: details Solution | ||
```haskell | ||
separate :: [Int] -> ([Int], [Int]) | ||
separate [] = ([], []) | ||
separate [x] = ([x], []) | ||
separate (x:y:xs) = let (evs, ods) = separate xs | ||
in (x:evs, y:ods) | ||
``` | ||
::: | ||
|
||
## Exercise 2 | ||
Write a function `numToStr :: Int -> Int -> String` taking as input an integer `n` together with a `radix` denoting the number of symbols used to represent the number `n` (for example 2,10,16 for binary, decimal, hexadecimal representation respectively). This function returns a string containing the representation of `n` in the corresponding numerical system. For the representation, use the standard symbols `0123456789ABCDEF`. | ||
|
||
Examples: | ||
```haskell | ||
numToStr 52 10 => "52" | ||
numToStr 5 2 => "101" | ||
numToStr 255 16 => "FF". | ||
``` | ||
|
||
::: tip Hint | ||
The representation can be obtained by consecutive division of `n` by `radix` and collecting the remainders. The integer division can be computed by the function `div` and the remainder after integer division can be computed by the function `mod`. | ||
::: | ||
|
||
|
||
::: details Solution | ||
```haskell | ||
numToStr :: Int -> Int -> String | ||
numToStr n radix = if n < radix then [chars !! n] | ||
else (numToStr d radix) ++ [chars !! r] | ||
where chars = ['0'..'9'] ++ ['A'..'F'] | ||
d = n `div` radix | ||
r = n `mod` radix | ||
``` | ||
::: | ||
|
||
## Exercise 3 | ||
Write a function `split n xs` that takes a natural number `n` and a list `xs :: [Int]` and splits `xs` into a list of | ||
lists of `n`-many consecutive elements. The last chunk of numbers can be shorter than `n`. E.g. | ||
```haskell | ||
split 3 [1..10] => [[1,2,3],[4,5,6],[7,8,9],[10]] | ||
split 3 [1,2] => [[1,2]] | ||
``` | ||
Use the function `split` to implement a function `average_n n xs` taking a list of integers and returning the list of the averages of `n` consecutive elements. | ||
E.g. | ||
```haskell | ||
average_n 3 [-1,0,1,2,3] => [0.0,2.5] | ||
``` | ||
|
||
::: tip Hint | ||
You can use functions `take n xs` and `drop n xs`. The first one returns the list of the first `n` elements of `xs`. The second returns the remaining list after stripping the first `n` elements off. Further, use function `length xs` returning the length of `xs`. | ||
::: | ||
|
||
|
||
The function `split` can be written recursively. If the length of `xs` is less than or equal to `n`, then return just `[[xs]]`. | ||
If it is bigger, then take the first `n` elements and cons them to the result of the recursive call of `split` after dropping the first `n` elements. | ||
|
||
::: details Solution | ||
```haskell | ||
split :: Int -> [Int] -> [[Int]] | ||
split n xs | (length xs) <= n = [xs] | ||
| otherwise = take n xs : (split n (drop n xs)) | ||
``` | ||
::: | ||
|
||
The function `average_n` can be easily written via the list comprehension using `split`. The only caveat is the division operation involved in the computation of averages. Even though the inner lists after applying `split` are of the type `[Int]`, their averages are floating numbers. So the type of `average_n` is `Int -> [Int] -> [Float]`. We can compute the sum of an inner list by the function `sum` and its length by `length`, but the type system would complain if we want to divide them. One must convert the integer arguments into floating-point numbers to overcome this problem. This can be done by the function `fromIntegral` converting an integer into any more general numeric type. | ||
|
||
::: details Solution | ||
```haskell | ||
average_n :: Int -> [Int] -> [Float] | ||
average_n n ys = [fromIntegral (sum xs) / fromIntegral (length xs) | xs <- xss] | ||
where xss = split n ys | ||
``` | ||
::: | ||
|
||
## Task 1 | ||
Write a function `copy :: Int -> String -> String` that takes an integer `n` and a string `str` and returns | ||
a string consisting of `n` copies of `str`. E.g. | ||
|
||
```haskell | ||
copy 3 "abc" => "abcabcabc" | ||
``` | ||
|
||
<!-- | ||
::: details Solution | ||
```haskell | ||
copy :: Int -> String -> String | ||
copy n str | n <= 0 = "" | ||
| otherwise = str ++ copy (n - 1) str | ||
-- tail recursive version | ||
copy2 :: Int -> String -> String | ||
copy2 n str = iter n "" where | ||
iter k acc | k <= 0 = acc | ||
| otherwise = iter (k-1) (acc ++ str) | ||
``` | ||
::: | ||
--> | ||
|
||
## Task 2 | ||
The Luhn algorithm is used to check bank card numbers for simple errors such as mistyping a | ||
digit, and proceeds as follows: | ||
* consider each digit as a separate number; | ||
* moving left, double every other number from the second last, e.g., 1 7 8 4 => 2 7 16 4; | ||
* subtract 9 from each number that is now greater than 9; | ||
* add all the resulting numbers together; | ||
* the card number is valid if the total is divisible by 10. | ||
|
||
Define a function `luhnDouble :: Int -> Int` that doubles a digit and subtracts 9 if the result is | ||
greater than 9. For example: | ||
```haskell | ||
luhnDouble 3 => 6 | ||
luhnDouble 7 => 5 | ||
``` | ||
|
||
Using `luhnDouble` and the integer remainder function `mod`, define a function | ||
`luhn :: [Int] -> Bool` that decides if a list of numbers representing a bank card number is valid. For | ||
example: | ||
```haskell | ||
luhn [1,7,8,4] => True | ||
luhn [4,7,8,3] => False | ||
``` | ||
|
||
::: tip Hint | ||
Since the numbers are processed from right to left, reverse first the list by the function `reverse`. Then apply the function `separate` from Exercise 1 to split the list into the numbers | ||
to be luhnDoubled and the rest. | ||
::: | ||
|
||
<!-- | ||
::: details Solution | ||
```haskell | ||
luhnDouble :: Int -> Int | ||
luhnDouble n | n > 4 = 2*n - 9 | ||
| otherwise = 2*n | ||
luhn :: [Int] -> Bool | ||
luhn xs = (sum evs + sum [luhnDouble x | x <- ods]) `mod` 10 == 0 | ||
where rxs = reverse xs | ||
(evs, ods) = separate rxs | ||
``` | ||
::: | ||
--> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.