We’ve just finished covering the B language.

Now we’re going to look at the *N* language, which deals with natural numbers.

The code for *N* is available here.

This is going to be a relative short tour, since you’ve seen most of this before. The important points are that we’ll be dealing with inductively defined values, and we’ll be looking briefly at the difference between strict and lazy evaluation.

The natural numbers are defined as:

- , for the number zero
- , for the successor of the number

The terms of *N* are as follows:

We are including here, which represents the predecessor of . Since we don’t have negative numbers, we define .

We can easily create a `Term`

type in Haskell:

```
data Term =
TmZero
| TmSucc Term
| TmPred Term
```

We’ve already mentioned that the natural numbers are either zero or the successor of a natural number. These will be the form of the values of *N*.

For the zero case, we have:

and:

```
valueTmZero :: Term
-> Maybe Term
valueTmZero TmZero =
Just TmZero
valueTmZero _ =
Nothing
```

For the successor case, we have:

and:

```
valueTmSucc :: (Term -> Maybe Term)
-> Term
-> Maybe Term
valueTmSucc val (TmSucc tm) =
TmSucc <$> val tm
valueTmSucc _ _ =
Nothing
```

We have four small-step rules: two of them are reduction rules, and two of them are congruence rules.

The reduction rules define the predecessor function.

For `pred O`

we have:

and:

```
ePredZero :: Term
-> Maybe Term
ePredZero (TmPred TmZero) =
Just TmZero
ePredZero _ =
Nothing
```

For `pred (S n)`

we have:

and:

```
ePredSucc :: Term
-> Maybe Term
ePredSucc (TmPred (TmSucc tm)) =
value tm
ePredSucc _ =
Nothing
```

The two congruence rules deal are used to keep things moving on when `S`

and `pred`

are wrapped around something other than a value.

The rule for `S`

is:

which corresponds to:

```
eSucc :: (Term -> Maybe Term)
-> Term
-> Maybe Term
eSucc step (TmSucc tm) = do
tm' <- step tm
return $ TmSucc tm'
eSucc _ _ =
Nothing
```

and the rule for `pred`

is:

which corresponds to:

```
ePred :: (Term -> Maybe Term)
-> Term
-> Maybe Term
ePred step (TmPred tm) = do
tm' <- step tm
return $ TmPred tm'
ePred _ _ =
Nothing
```

The rules we have seen so far are for strict evaluation.

The usual distinction between strict and non-strict is related to whether evaluation continues inside of function abstraction or not.

We haven’t covered functions yet, but we now have something similar. Recall that constructors in Haskell are functions, and that natural numbers would be represented by:

```
data Nat =
O
| S Nat
```

so we have a function

`S :: Nat -> Nat`

With strict evaluation we evaluate the arguments to `S`

- using `V-Succ`

and `E-Succ`

- when we come across `S n`

as the top-level term.

With lazy evaluation we don’t evaluate the argument to `S`

in either of those cases. The rule `E-PredSucc`

can still move things forward when we have a `S`

inside of one of our terms, but the outer ’S’s are left alone.

This means that for lazy evaluation we completely delete the `E-Succ`

rule above and rely on the other rules to peek inside of the `S`

constructor.

We also need to update the `V-Succ`

rule so that it doesn’t look inside of the `S`

constructor, and so we have:

and:

```
valueTmSucc :: Term
-> Maybe Term
valueTmSucc (TmSucc tm) =
Just (TmSucc tm)
valueTmSucc _ =
Nothing
```

For now we’ll stick to strict evaluation, but we’ll come back to lazy evaluation later in the series.

From this point, we just need to write the code for `QuickCheck`

support, parsing and printing for *N* and we’re done.

And that’s all we need to do. If we copy the tests and the REPL across from the *B* project into the *N* project, they’ll still work.

That’s partly due to using the same interface, but also partly due to the form and robustness of the PLT theorems that we’re using for our properties.

We are going to look at more uni-typed language before we add some new concepts into the mix.

- Complete the
`QuickCheck`

, parsing and printing for*N*. - Devise semantics for
*I*, with terms for integer literals,`+`

,`-`

,`*`

and`^`

. - Implement
*I*in Haskell, including the semantics,`QuickCheck`

, parsing and pretty-printing.

Site proudly generated by Hakyll

This work is licensed under a Creative Commons Attribution 4.0 International License