A quick peek at GimML – Website of project agreg

Here are a few things you can write in GimML.

The following declares a type of first-order terms, where application is written using an infix operator $ (the 0 in the declaration infix 0 $ declares it with precedence 0, but let us skip that). This is just as in Standard ML. A term is either a variable, for example V "x" (standing for x), or an application, say "f" $ [V "x"] (standing for f(x)).

infix 0 $

datatype term = V of string
              | $ of string * term listi

Now here is something particular to GimML. A substitution theta is a map from variable names (of type string) to terms. A GimML map is just a table: you may think of it as a hash table; if you are more mathematically minded, it is a function with finite domain.

It is easy to define a substitution function tsubst, which applies a substitution theta to a term t. I will give the definition below. Its type is:

tsubst : (string -m> term) -> term -> term

Note that the type of maps from string to term is written with the map arrow operator -m>. Let us apply it to an example. We define two constants a and b, two helper functions that build applications of function symbols f and grespectively, then two terms t1 and t2. theta is our first substitution!

val a = "a" $ [];             (* the constant a *)
val b = "b" $ [];             (* the constant b *)
fun f (s, t) = "f" $ [s, t];  (* applying the binary function symbol f *)
fun g (t) = "g" $ [t];        (* applying the unary function symbol g *)
val t1 = f (a, g (a));        (* a first term *)
val t2 = f(a,f(b,g(f(a,b)))); (* a second term *)
val theta = {"x" => t1, "y" => t2};    (* a substitution *)

Now can you guess what the following term will evaluate to?

tsubst theta (f (V "x", V "y"));

Try it under the GimML toplevel, and compare that to the expected term f (t1, t2) = f(f(a,g(a)), f(a,f(b,g(f(a,b))))).

Oh, and here is the definition of tsubst, in case you would like to see how it is done.

fun tsubst (theta : string -m> term) =
    let fun tsubst_theta (V x) =
            if x inset theta         (* if x is in the domain of theta *)
               then ?theta x         (* read off the value associated with x in theta, *)
            else V x                 (* else return the variable itself *)
          | tsubst_theta (f $ l) =
            f $ [tsubst_theta t | t in list l] (* list comprehension *)
    in
       tsubst_theta
    end;