The "nominal_datatype" API (preliminary work)

[binghe]

Hi,

This is a preliminary work (first step) of establishing a user-friendly API for creating nominal datatypes. Currently it's not easy to create them - a lot of boilerplate code must be written. Now I added a function nominal_datatype (in nomdatatype) to automate the initial part of this process. Let me first introduce the API.

For the type term (of λ-calculus), now user can use the following call to create a nominal type term representing λ-terms with constructors VAR, APP and LAM:

val {tynames, rep_t, lp} =
    nominal_datatype ‘term = VAR 'free | APP term term | LAM 'bound term’;

Note that the special type variables 'free and 'bound to denote free and bound names used in the related constructors. Other type variables and parameterized types are considered external types. The above call currently returns 3 values (and a Datatype call happens inside):

• tynames is a list of names of the nominal types being created. The value is ["term"] in this case.
• rep_t is the intermediate representation type, whose value is :term_repcode, defined automatically by

Datatype :
   term_repcode = rVAR | rAPP | rLAM
End

• lp is a long term holding information about the number of free and bounded names and recursive arguments:

   ``\n lfvs d tns uns.
         n = 0 /\ lfvs = 1 /\ d = rVAR /\ tns = [] /\ uns = [] \/
         n = 0 /\ lfvs = 0 /\ d = rAPP /\ tns = [] /\ uns = [0; 0] \/
         n = 0 /\ lfvs = 0 /\ d = rLAM /\ tns = [0] /\ uns = []``: term

That's all it currently can do. Perhaps it's not very impressive for the type term. But for the two nominal terms of π-calculus, we can do the following now: (NOTE: setting repcode will forcely set the type name of the representation type, otherwise it's pi_repcode by default.)

val _ = (repcode := "repcode");

val {tynames, rep_t, lp} =
    nominal_datatype
          ‘pi   = Nil                         (* 0 *)
                | Tau pi                      (* tau.P *)
                | Input 'free 'bound pi       (* a(x).P *)
                | Output 'free 'free pi       (* {a}b.P *)
                | Match 'free 'free pi        (* [a == b] P *)
                | Mismatch 'free 'free pi     (* [a <> b] P *)
                | Sum pi pi                   (* P + Q *)
                | Par pi pi                   (* P | Q *)
                | Res 'bound pi               (* nu x. P *)
                ;
       residual = TauR pi                     (* tau.P *)
                | InputS 'free 'bound pi      (* a(x).P *)
                | BoundOutput 'free 'bound pi (* a{x}.P *)
                | FreeOutput 'free 'free pi   (* {a}b.P *)’;

And this will give us the following correct lp term, which previously must be written manually:

val lp =
  “(\n lfvs d tns uns.
     n = 0 /\ lfvs = 0 /\ d = rNil /\ tns = [] /\ uns = [] \/
     n = 0 /\ lfvs = 0 /\ d = rTau /\ tns = [] /\ uns = [0] \/
     n = 0 /\ lfvs = 1 /\ d = rInput /\ tns = [0] /\ uns = [] \/
     n = 0 /\ lfvs = 2 /\ d = rOutput /\ tns = [] /\ uns = [0] \/
     n = 0 /\ lfvs = 2 /\ d = rMatch /\ tns = [] /\ uns = [0] \/
     n = 0 /\ lfvs = 2 /\ d = rMismatch /\ tns = [] /\ uns = [0] \/
     n = 0 /\ lfvs = 0 /\ d = rSum /\ tns = [] /\ uns = [0; 0] \/
     n = 0 /\ lfvs = 0 /\ d = rPar /\ tns = [] /\ uns = [0; 0] \/
     n = 0 /\ lfvs = 0 /\ d = rRes /\ tns = [1] /\ uns = [] \/
     n = 1 /\ lfvs = 0 /\ d = rTauR /\ tns = [] /\ uns = [0] \/
     n = 1 /\ lfvs = 1 /\ d = rInputS /\ tns = [0] /\ uns = [] \/
     n = 1 /\ lfvs = 1 /\ d = rBoundOutput /\ tns = [0] /\ uns = [] \/
     n = 1 /\ lfvs = 2 /\ d = rFreeOutput /\ tns = [] /\ uns = [0])”;

Note that, I have reused the input syntax of the existing Datatype package, and for labelled term there's no way to distinguish between free and bound parameters:

val _ = (repcode := "lrep");
val _ = (rprefix := "l");

val {tynames, rep_t, lp} =
    nominal_datatype
      ‘lterm = VAR 'free
             | APP lterm lterm
             | LAM 'bound lterm
             | LAMi num 'bound lterm lterm’;

which gives the following lp:

val lp = “λn lfvs (d:lrep) tns uns.
            n = 0 /\ lfvs = 1 /\ d = lVAR /\ tns = [] /\ uns = [] \/
            n = 0 /\ lfvs = 0 /\ d = lAPP /\ tns = [] /\ uns = [0;0] \/
            n = 0 /\ lfvs = 0 /\ d = lLAM /\ tns = [0] /\ uns = [] \/
            ?m. n = 0 /\ lfvs = 0 /\ d = lLAMi m /\ tns = [0] /\ uns = [0]”;

Note that LAMi num 'bound lterm lterm actually means (LAMi num 'bound lterm) lterm, where the first lterm is bounded by the name, while the second is not. And that's why the last line of lp has tns = [0] /\ uns = [0], i.e. one parameter is free, the other is bound.

The current rule (to interprete the input quotation) is the following: if the type variable'bound occurs in a constructor, then the immediately followed nominal type parameter is bounded, while other nominal parameters are considered free. This avoids designing new syntax of the input quotation for now and works for all existing use cases.

--Chun

[mn200]

Thanks!