Algebra

[jmikedupont2]

Here is how we can formalize a simple expression algebra with addition and multiplication for integers 1-10 using UniMath:

First, we define the signature with two operations:

Definition expr_signature : signature :=
  ((unit ; nat), 
   [( [nat; nat]; nat); // binary addition 
    ([nat; nat]; nat)]) // binary multiplication

We have one sort, nat, for integer values. Two operators for addition and multiplication, both taking two nat arguments.

Next we define the algebra using the standard nat operations in UniMath:

Definition nat10 : hSet := settrunc (λn : nat, leq 1 n ∧ leq n 10).

Definition expr_algebra : algebra expr_signature := 
 ([(nat10)], 
  [(λxy : nat10×nat10, x + y);  
   (λxy : nat10×nat10, x * y)])

We truncate the naturals to get a subset from 1-10. The algebra interprets the operators as regular addition and multiplication on this set.

Now we can build terms over this signature using variables, constants, and the two operations. For example:

Definition x : term _ _ := varterm 0.
Definition y : term _ _ := varterm 1.
Definition three : term _ _ := build_term (•0 : names expr_signature) [3]. 

Definition ex1 : term _ _ := 
  build_term (•1) [x ; three] // x * 3

We have defined variables x,y; constant 3; and term x*3. We can evaluate terms by interpreting into the expr_algebra.

This shows how basic expression manipulation can be modeled using the UniMath algebra framework in a simple way. We get operations, variables, and term construction for free!

[jmikedupont2]

Here is one way we can lift the OCaml AST for type declarations to a Universal Algebra structure in UniMath:

First, we define a signature for type declarations:

Definition tdecl_signature : signature :=
  ((unit ; typecat) ;  // types category
   (unit ; string) ;  // constructor names
   list typecat ;     // constructor args
   string) ;          // type names

Definition tdecl_ops : ∏ s : tdecl_signature, 
      algebra tdecl_signature  
| [_ , _ , tt , _ ] → // types
  mk_typecat int string float // base types
| [_ , c , _ , _ ] →  
  string // constructor names
| [_ , _ , args , _ ] →
  listset typecat // args are lists
| [res, _ , _ , _] →
  stringset // type names   

We have separate sorts for:

• base types (int, string etc.)
• constructor names
• argument lists
• declared type names

Now we can define the AST as an algebra:

Definition my_tdecl : algebra tdecl_signature :=
  mk_algebra (lam s, match s with
     | tt => typecatset 
     | _ => stringset
   end)  
   tdecl_ops

Definition my_type :@ term _ _ my_tdecl _ tt = 
  "my_type" // name

Definition my_ctor : @ term _ _ my_tdecl _ string =
  "MyType" // constructor name

Definition my_args : @ term _ _ my_tdecl (list typecat) tt =
  [int_type; string_type; float_type] // arg list

This models the previous AST using theUniMath algebra framework in a structured way.

We can go further by adding typechecking rules and other operations on declarations using the equation solver capabilities.