Library PSLC

Basic source-level lambda calculus with naturals, products, and sums

Require Import List.

Require Import Binding.

Set Implicit Arguments.

The language


We start by defining the language of data types in a very straightforward way.
Inductive dty : Set :=
  | Nat : dty
  | Prod : dty -> dty -> dty
  | Sum : dty -> dty -> dty.

Next are the types in general.
Inductive ty : Set :=
  | Data : dty -> ty
  | Arrow : ty -> ty -> ty.

Here is the language of terms. The type family term is parameterized by a Debruijn-indexed typing context and type that appear in the typing judgment for a particular term. The type Var is a generic Debruijn variable type defined in Binding.
Inductive term : list ty -> ty -> Set :=
  | EVar : forall G t,
    Var G t
    -> term G t
  | Lam : forall G dom ran,
    term (dom :: G) ran
    -> term G (Arrow dom ran)
  | App : forall G dom ran,
    term G (Arrow dom ran)
    -> term G dom
    -> term G ran

  | Const : forall G, nat -> term G (Data Nat)

  | Pair : forall G t1 t2,
    term G (Data t1)
    -> term G (Data t2)
    -> term G (Data (Prod t1 t2))
  | Fst : forall G t1 t2,
    term G (Data (Prod t1 t2))
    -> term G (Data t1)
  | Snd : forall G t1 t2,
    term G (Data (Prod t1 t2))
    -> term G (Data t2)

  | Inl : forall G t1 t2,
    term G (Data t1)
    -> term G (Data (Sum t1 t2))
  | Inr : forall G t1 t2,
    term G (Data t2)
    -> term G (Data (Sum t1 t2))
  | Case : forall G t1 t2 t,
    term G (Data (Sum t1 t2))
    -> term (Data t1 :: G) t
    -> term (Data t2 :: G) t
    -> term G t.

Denotational semantics


We compile data types into their natural Coq Set counterparts.
Fixpoint dtyDenote (t : dty) : Set :=
  match t with
    | Nat => nat
    | Prod t1 t2 => (dtyDenote t1 * dtyDenote t2)%type
    | Sum t1 t2 => (dtyDenote t1 + dtyDenote t2)%type
  end.

Likewise for types in general
Fixpoint tyDenote (t : ty) : Set :=
  match t with
    | Data t => dtyDenote t
    | Arrow t1 t2 => tyDenote t1 -> tyDenote t2
  end.

Term denotation is further parameterized by a substitution assigning values to all free variables. The generic type Subst is from Binding. It is parameterized first, by a denotation function explaining what type of value we want to include for each type in the typing context; and second, by the actual typing context to use.
Fixpoint termDenote (G : list ty) (t : ty) (e : term G t) {struct e}
  : Subst tyDenote G -> tyDenote t :=
  match e in (term G t) return (Subst tyDenote G -> tyDenote t) with
    | EVar _ _ v => VarDenote v
    | Lam _ _ _ e' => fun s x => termDenote e' (SCons _ x s)
    | App _ _ _ e1 e2 => fun s => (termDenote e1 s) (termDenote e2 s)

    | Const _ n => fun _ => n

    | Pair _ _ _ e1 e2 => fun s => (termDenote e1 s, termDenote e2 s)
    | Fst _ _ _ e => fun s => fst (termDenote e s)
    | Snd _ _ _ e => fun s => snd (termDenote e s)

    | Inl _ _ _ e1 => fun s => inl _ (termDenote e1 s)
    | Inr _ _ _ e2 => fun s => inr _ (termDenote e2 s)
    | Case _ t1 t2 _ e e1 e2 => fun s =>
      match termDenote e s with
        | inl e' => termDenote e1 (SCons (denote:= tyDenote) (Data t1) e' s)
        | inr e' => termDenote e2 (SCons (denote:= tyDenote) (Data t2) e' s)
      end
  end.

Index
This page has been generated by coqdoc