---
title: fibonacci in maude and ats
date: 2022-10-24
tags: [computer, maude, ATS]
...

i might submit these [here], if i can be bothered to get a new github account.

[here]: https://braxtonhall.ca/fib/

:::aside
update: i did it
:::


# maude

```maude
smod FIB is
  pr LIST{Nat} .

  vars M N : Nat .
  var  Ns  : List{Nat} .

  rl [start]: nil => 0 1 .
  rl [next]:  Ns M N => Ns M N (M + N) .
  rl [drop]:  Ns N => N .

  strats fib fibgo : Nat @ List{Nat} .
  sd fib(N)      := start ; fibgo(N) .
  sd fibgo(0)    := top(drop) .
  sd fibgo(s(N)) := top(next) ; fibgo(N) .
endsm
```

```
Maude> srew nil using fib(10) .
srewrite in FIB : nil using fib(10) .

Solution 1
rewrites: 8330 in 12ms cpu (12ms real) (694166 rewrites/second)
result NzNat: 89

No more solutions.
rewrites: 8469 in 12ms cpu (13ms real) (705750 rewrites/second)
```


# ats

```ats
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

// is_fib(i, n): n is the i-th fibonacci number
dataprop is_fib(int, int) =
| F0(0, 0) | F1(1, 1)
| {i, m, n : nat} Fplus(i + 2, m + n) of (is_fib(i, m), is_fib(i + 1, n))

typedef fib(i : int) = [n : nat] (is_fib(i, n) | int(n))

fun fib {t : nat} .<>. (t : int(t)) :<> fib(t) =
let
  // m, n : accs
  // i : index of m
  // t : target index
  fun go {m, n, i, t : nat | i <= t} .<t - i>.
         (M : is_fib(i, m), N : is_fib(i + 1, n) |
          m : int(m), n : int(n), i : int(i), t : int(t)) :<>
        fib(t) =
    if i = t then
      (M | m)
    else
      go(N, Fplus(M, N) | n, m + n, i + 1, t)
in
  go(F0, F1 | 0, 1, 0, t)
end

fun fib_(i : Nat) : Nat = let val (_ | res) = fib(i) in res end

implement main0() = println!("fib(15) = ", fib_(15))
```

```sh
$ make fib
$ ./fib
fib(15) = 610
```

same makefile as [last time].

[last time]: ./2022-09-16-ats.html#install