PUBS: A Practical Upper Bounds Solver
```
(* * * * * * * * * * *
* Resource Aware ML *
* * * * * * * * * * *
*
* File:
*   longestCommonSubsequence.raml
*
* Author:
*   Jan Hoffmann (2010)
*
* Resource Bound:
*   O(n*m)
*
* Description:
*   A standard example of dynamic programming that can be found in
*   many textbooks (see e.g. Cormen/Leiserson/Rivest/Stein:
*   Introduction to Algorithms) is the computation of the length of
*   the longest common subsequence (LCS) of two given lists
*   (sequences).  Given two sequences a_1,...,a_n and b_1,...,b_m, one
*   successively fills an nxm-matrix (here a list of lists) A such
*   that A(i,j) contains the length of the LCS of a_1,...,a_i and
*   b_1,...,b_j.  It is the case that
*
*            { 0                      if i=0 or j=0
*   A(i,j) = { A(i-1,j-1) + 1         if i,j > 0 and a_i = b_j
*            { max(A(i,j-1),A(i-1,j)) if i,j > 0 and a_i \= b_j
*
*   This algorithm can be analyzed in our system and is exemplary for
*   similar algorithms that use dynamic programming.
*)

lcs : (L(int),L(int)) -> int
(* computes the length of the longest common subsequence *)

lcs(l1,l2) = let _=tick(1) in
let m = lcstable(l1,l2) in
match m with
| nil -> +0
| (l1::_) -> match l1 with
| nil -> +0
| (len::_) -> len;

(*
eq(lcs(A,B),1,[lcstable(A,B)],[A>=0,B>=0]).
*)

lcstable : (L(int),L(int)) -> L(L(int))
(* computes the table of lengths *)

lcstable (l1,l2) = let _=tick(1) in
match l1 with
| nil -> [firstline l2]
| (x::xs) -> let m = lcstable (xs,l2) in
match m with
| nil -> nil
| (l::ls) -> (newline (x,l,l2))::l::ls;

(*
eq(lcstable(A,B),1,[firstline(B)],[A=0]).
eq(lcstable(A,B),1,[newline(X,B,B),lcstable(Ap,B)],[A>=1,Ap=A-1]).

eq(out1_lcstable(A,B),1,[],[A=0]).
eq(out1_lcstable(A,B),1,[out1_lcstable(Ap,B)],[A>=1,Ap=A-1]).

eq(out2_lcstable(A,B),nat(B),[],[A=0]).
eq(out2_lcstable(A,B),0,[out2_lcstable(Ap,B)],[A>=1,Ap=A-1]).
*)

firstline : L(int) -> L(int)
(* Returns the first line of zeros *)

firstline(l) =  let _=tick(1) in
match l with
| nil -> nil
| (x::xs) -> +0::firstline xs;

(*
eq(firstline(A),1,[],[A=0]).
eq(firstline(A),1,[firstline(Ap)],[A >=1,Ap=A-1]).
*)

newline : (int,L(int),L(int)) -> L(int)
(* computes a new line according to the recursive definition above
* y is the element of the second list
* lastline the the previously computed line in the matrix
* l contains elements of the first list *)

newline (y,lastline,l) = let _=tick(1) in
match l with
| nil     -> nil
| (x::xs) -> match lastline with
| nil -> nil
| (belowVal::lastline') ->
let nl = newline(y,lastline',xs) in
let rightVal = right nl in
let diagVal =  right lastline' in
let elem = if x == y then diagVal+1 else max(belowVal,rightVal)
in elem::nl;

(*
eq(newline(A,B,C),1,[],[C=0]).
eq(newline(A,B,C),1,[],[C>=1,B=0]).
eq(newline(A,B,C),1,[right(Cp),right(Bp),max(E,F),newline(A,Bp,Cp)],[C>=1,B>=1,Bp=B-1,Cp=C-1]).
eq(newline(A,B,C),1,[right(Cp),right(Bp),newline(A,Bp,Cp)],[C>=1,B>=1,Bp=B-1,Cp=C-1]).

eq(out_newline(A,B,C),0,[],[C=0]).
eq(out_newline(A,B,C),0,[],[C>=1,B=0]).
eq(out_newline(A,B,C),1,[out_newline(A,Bp,Cp)],[C>=1,B>=1,Bp=B-1,Cp=C-1]).
*)

right : L(int) -> int

right l =  let _=tick(1) in
match l with
| nil -> +0
| (x::xs) -> x;
(*
eq(right(A),1,[],[]).
*)
max : (int,int) -> (int)

max (a,b) = let _=tick(1) in
if a>b then a else b;
(*
eq(max(A,B),1,[],[]).
*)

```