\documentclass[11pt]{book}

%include lhs2TeX.fmt
%include polycode.fmt

\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{stmaryrd}
\usepackage{float}
\usepackage{mathpartir}
\usepackage{xcolor}
\usepackage{natbib}
\usepackage[pdftex]{graphicx}

\floatstyle{boxed}
\restylefloat{figure}

\author{Arie Middelkoop}
\title{Semantics For Ruler}

%format ^   = " "
%format ^^  = "\;"
%format ^^^ = "\hspace{1em}"
%format ^^^^ = "\hspace{4em}"
%format (overline (x)) = "\overline{" x "}"
%format .   = "."
%format mid = "|"
%format ::= = "::="
%format :=  = ":="
%format e1
%format e2
%format Ctx = "\mathcal{E}\!\!"
%format Ctx1
%format Ctx2
%format H1
%format H2
%format (sub x (s)) = "{" x "}_{" s "}"
%format :-> = "\mapsto"
%format rec = "\mathbf{rec}"
%format env = "\Gamma"
%format env1
%format env'
%format ty  = "\tau"
%format ty1
%format ty2
%format ty3
%format ty4
%format ts = "\sigma"
%format ts1
%format ts2
%format ts3
%format ts4
%format j1
%format j2
%format :- = "\vdash"
%format ::- = "\Vdash"
%format forall = "\forall\!"
%format alpha = "\alpha"
%format CC = "\mathcal{C}"
%format empty = "\emptyset"
%format exists = "\exists\!"
%format union = "\cup"
%format def = ::=
%format phi = "\Phi"

%format LambdaExp = "\lambda^{\tau}"


\newcommand\HRules{\scshape HRules\normalfont}
\newcommand\NRules{\scshape NRules\normalfont}
\newcommand\Ruler{\scshape Ruler\normalfont}


\begin{document}

\chapter{Denotational Semantics For \Ruler}

  \section{Notation}

  We use the follow notation extensively in this chapter:

  \begin{code}
  overline(x)                         -- a (possibly ordered) set of x
  empty                               -- the empty set
  x                                   -- singleton set containing x
  x # y                               -- intersection |x| and |y| empty
  [x := y] z                          -- substitute |y| for |x| in |z|
  [(overline(x)) := (overline(y))] z  -- simultaneous pairwise substitution
  \end{code}

\section{Type Rule Language \HRules}

  We introduce a language for type rules with higher-order typing relations.
  This is a simpler variation on $\lambda$Prolog.

\subsection{Semantics}

  A higher-order type system in \HRules{} is a set of clauses |X|.
  The grammar for clauses is given by the following productions:
  \begin{code}
  q  def  forall (overline x) ^^ . ^^ c             -- quantified clause
  c  def  (overline j) ^^ ; ^ j                     -- clause
  j  def  x (overline x)                            -- judgment
  \end{code}
  with identifiers |x|. A clause consists of judgments as premisses and
  one conclusion judgment, and is quantified over some of its variables.
  A judgment is made up by a variable |x| representing a relation,
  and its terms in the form of variables |overline x|. Relations are first
  class and can take other relations as parameter. Hence, we take an intentional
  view on both terms and relations by representing them by variables, and their
  properties with judgments.

  Given a type system |X|, informally, a judgment |j| is satisfied if it can be
  reduced to satisfyable judgments by a clause in |X|. Formally,
  |j| is satisfied if there exists a derivation |:- j|, specified by the
  following inference rule:
  \begin{mathpar}
  \inferrule*[right=reduce]
    { |(forall (overline z) ^^ . ^^ [(overline(z')) := (overline(z))] (j1, ..., (sub j k) ; r (overline(y)))) `elem` X| \\
      |fv (sub j i) # (overline(x))| \\
      | :- [(overline(y)) := (overline(x))] (sub j i)| \\
    }
    { |:- r (overline(x))| }
  \end{mathpar}
  with the free variables of a judgment j, written as |fv j|, defined as:
  \begin{code}
  fv (x (overline x)) = {x} union (overline x)
  \end{code}
  With the $\TirName{reduce}$ rule, a judgment is decomposed in
  smaller judgments if there is a clause with a matching conclusion in the clause set. Note
  that variables |(overline(z'))| have to be chosen carefully, and are used for
  alpha conversion of the clause in question. The requirement that the free variables in all
  judgments may not overlap with the substitutes, ensures a capture avoiding substitution.
  Clauses with an empty set of premisses take the role of assumptions.
  
  We represent extensional terms intentionally as variables. Consider terms in an
  extensional way, given by the grammar:
  \begin{code}
  t  def  F((sub t 1), ..., (sub t k))  -- term
  \end{code}
  with a function symbol |F| of arity |k|.
  Intentionally, we represent a term |t| as a variable, say |x|, together with a
  clause |empty ; f x (sub x 1) ... (sub x k)|, where |f| is the intentional
  representation of the relation that states that |t| is an |F|-term of terms
  intentionally represented by |(sub x 1), ..., (sub x k)| respectively.
  Opaque terms (i.e. terms that have no inspectable structure) are represented
  only as a variable.

  \subsection{Example}

  We demonstrate the type system of the simply-typed lambda calculus in \HRules{}.
  First the syntax of terms and their corresponding intentional encoding:
  \begin{code}
  e    def  x                    evar e x                  -- var
       mid  e1 e2                eapp e e1 e2              -- app
       mid  \x.e                 elam e e1 e2              -- lam
  ^
  ty   def  ty -> ty             tarr ty ty1 ty2           -- arrow
  env  def  x :: ty, env1  ^^^^  ext env x ty env1   ^^^^  -- extend
  ^
  env :- e : ty                  tc env e ty               -- tc judgment
  (x :: ty) `elem` env           lookup x ty env           -- lookup judgment
  \end{code}
  Note that |e1| is some expression when considered as a term, but a variable
  when considering them intentionally. For example, the lambda term |\x.(\y. x y)|,
  represented intentionally as the variable |e1|, is accompanied by the
  following clauses:
  \begin{code}
    empty ^^ ; ^^ elam e1 x1 e2  -- outermost lambda
    empty ^^ ; ^^ elam e2 y1 e3  -- innermost lambda
    empty ^^ ; ^^ eapp e3 e4 e5  -- |x y| application
    empty ^^ ; ^^ evar e4 x1     -- |x| variable
    empty ^^ ; ^^ evar e5 y1     -- |y| variable
    empty ^^ ; ^^ ident x1       -- |x| identifier
    empty ^^ ; ^^ ident y1       -- |y| identifier
  \end{code}

  For notational convenience, we write a clause:
  \begin{displaymath}
  |j1, ..., (sub j k) ^^ ; ^^  j| \hspace{4em}\mbox{as}\hspace{4em} \inferrule{|j1 ... (sub j k)|}{|j|}
  \end{displaymath}

  Bla.

  \begin{mathpar}
    \inferrule*[right=var]
      { |(x :: ty) `elem` env| }
      { |env :- x : ty| }

    \inferrule
      { |evar x| \\
        |lookup x ty env|
      }
      { |tc env x ty| }\\

    \inferrule*[right=app]
      { |env :- f : ty1 -> ty2| \\
        |env :- a : ty1|
      }
      {|env :- f a : ty2|}

    \inferrule
      { |eapp e f a| \\
        |tc env f ty3| \\\\
        |tc env a ty2| \\
        |tarr ty3 ty2 ty1|
      }
      { |tc env e ty1| }\\

    \inferrule*[right=lam]
      { |x :: ty1| \\
        |env :- e : ty2|
      }
      { |env :- \x.e : ty1 -> ty2| }

    \inferrule
      { |elam e x b| \\
        |ext env2 x ty2 env1| \\\\
        |tc env2 b ty3| \\
        |tarr ty1 ty2 ty3|
      }
      {|tc env1 e ty1|}
  \end{mathpar}
  
  \subsection{Static Semantics}
  
  Do not confuse this with the example of the previous subsection!

  \begin{code}
  env  def  (overline (x :: ty))               -- identifier environment
  phi  def  (overline (ty :: (overline ty)))   -- relation environment
  ^
  phi ; env :- j                               -- judgment |j| is well typed in |phi| and |env|
  phi ; env :- c                               -- clause |c| is well typed in |phi| and |env|
  phi ; env :- q                               -- quantified clause |q| is well typed in |phi| and |env|
  \end{code}
  with identifiers |x| and |ty|.

  \begin{mathpar}
  \inferrule*[right=judge]
    { |(x :: ty) `elem` env| \\\\
      |(ty :: (overline ty)) `elem` phi| \\\\
      |((sub x i) :: (sub ty i)) `elem` env|
    }
    { |phi ^^ ; ^^ env :- x (overline x)| }

  \inferrule*[right=clause]
    { |(x :: ty) `elem` env| \\\\
      |(ty :: (overline ty)) `elem` phi| \\\\
      |phi ^^ ; ^^ (overline x) :: (overline ty), env :- (sub j i)|
    }
    { |phi ^^ ; ^^ env :- (overline j) ^^;^^ x (overline x)| }

  \inferrule*[right=quant]
    { |phi ^^ ; ^^ (overline z) :: (overline ty), env :- c| }
    { |phi ^^ ; ^^ env :- forall (overline z) ^^ . ^^ c| }
  \end{mathpar}

  Rule \TirName{quant} introduces types for the universally quantified variables.
  Rule \TirName{clause} introduces types for the goal variables.
  All variables must have a type, and thus must be introduced either way.

%if False
q  def  forall (overline x) ^^ . ^^ c             -- quantified clause
  c  def  (overline j) ^^ ; ^ j                   -- clause
  j  def  x (overline x)                          -- judgment
%endif

  \subsection{Properties}

  Consistent? Complete?

  \subsection{Embedding of lambda calculus}
  \subsection{Embedding of attribute grammars}



\section{Type Rule Language \NRules}

  We introduce a language for nested type rules, which is an extension of the
  language presented in the previous section.

  \subsection{Semantics}

  \begin{code}
  q  def  forall (overline x) ^^ . ^^ c             -- quantified clause
  c  def  (overline j) ^^ ; ^ g                     -- clause
  j  def  g                                         -- judgment
          { g }                                     -- judgment introducing a scope
          q                                         -- nested clause
  g  def  x xs                                      -- goal
  \end{code}



%if False

\chapter{Semantics For Ruler}

We define the semantics of a series of languages, starting with a familiar
lambda calculus and ending with |Ruler|.


\section{Explicitly typed Lambda Calculus: |LambdaExp|}

We introduce a variant of the lambda calculus, named |LambdaExp|.

Strict evaluation. If it works for strict evaluation, it also works while
using normal order reduction.


\subsection{Grammar}

  The grammar of |LambdaExp| consists of:
  \begin{code}
      -- values
    v    ::=  \(x :: ts) . e                  -- lambda
         mid  l                               -- label
         mid  CC (overline v)                 -- sat. constr. value
    ^
      -- expressions
    e    ::=  x                               -- variable
         mid  v                               -- value
         mid  C (overline e)                  -- sat. constr. expr.
         mid  e1 e2                           -- application
         mid  rec x = e1 in e2                -- recursive binding
         mid  case e of (overline a)          -- case expression
    ^
      -- case alternatives
    a    ::=  CC (overline v) -> e            -- case alternative
    ^
      -- type schemes
    ts   ::=  forall (overline alpha) . ty    -- quantified type
         mid  ty                              -- simple type
         mid  alpha                           -- variable
    ^
      -- types
    ty   ::=  ts -> ty                        -- arrow
         mid  T                               -- type constructor
  \end{code}
  with labels |l|, and identifiers |x|.

  An expression |e| is {\it proper} if:
  \begin{itemize}
  \item does not contain any labels |l|
  \item does not contain saturated constructor values |CC|
  \item All constructor expressions are of the form:
        |C (overline(x))|, with variables |(sub x 1), ..., (sub x k)|,
        and |k| the arity of |C|.
  \end{itemize}

\subsection{Operational Semantics}

  \begin{code}
      -- evaluation contexts
    Ctx  ::=  []                        -- hole
         mid  e Ctx                     -- application
         mid  rec x = Ctx in e          -- recursive binding
         mid  case Ctx of (overline a)  -- case expression
    ^
      -- heaps
    H    ::=  l :-> v, H                -- label to value mapping
    ^
      -- state
    S    ::=  (H ; e)                   -- execution state
    ^
    (H ; e) -> (H' ; e')                -- reduction
  \end{code}

  \begin{mathpar}
    \inferrule*[right=deref]
      {}
      { |(H ; l) -> (H ; H(l) )| }

    \inferrule*[right=con]
      {}
      { |(H ; Ctx[C (overline l)]) -> (H ; CC (overline l) )| }

    \inferrule*[right=beta]
      {\mbox{with |l| fresh}}
      { |(H ; (\(x :: ts) . e) v) -> (l :-> v, H ; [x := v] e )| }

    \inferrule*[right=let]
      {\mbox{with |l| fresh.}}
      { |(H ; rec x = v in e -> ( l :-> [x := l] v, H ; [x := l] e )| }

    \inferrule*[right=case]
      {\mbox{for some |i|, and |(sub a i) = C (overline x) -> (sub e i)|, with |(overline l)| fresh}}
      { |(H ; case (C (overline v)) of (overline a) ) -> ( (overline l) :-> (overline v), H ; [ (overline x) := (overline l) ] (sub e i) )| }

    \inferrule*[right=ctx]
      { |(H ; e) -> (H' ; e')| }
      { |(H ; Ctx[e]) -> (H' ; Ctx[e'])| }
  \end{mathpar}

  \subsection{Static Semantics}

  \begin{code}
      -- environments
    env  ::=  x  :: ts, env        -- variable type
         mid  C  :: ty, env        -- constructor type
         mid  l  :: ts, env        -- label type
    ^
    env :- e : ty                  -- type judgment
  \end{code}

  \begin{mathpar}
  \inferrule*[right=var]
    { |x :: forall (overline alpha) . ty `elem` env| }
    { |env :- x : [overline (alpha := ts)] ty| }

  \inferrule*[right=con]
    { |C :: ts1 -> ... -> (sub ts k) -> T `elem` env| \\
      |(sub x i) :: (sub ts i) `elem` env, ^^^ 1 <= i <= k|
    }
    { |env :- C (overline x) : T| }
  
  \inferrule*[right=lab]
    { |l :: forall (overline alpha) . ty `elem` env| }
    { |env :- l : [overline (alpha := ts)] ty| }

  \inferrule*[right=lam]
    { |x :: ts, env :- e : ty| }
    { |env :- \(x :: ts) . e : ts -> ty| }

  \inferrule*[right=app]
    { |env :- f : forall (overline alpha) . ty1 -> ty2| \\
      |env :- a : ty1| \\
      |(overline alpha) # ftv(env)|
    }
    { |env :- f a : ty2| }

  \inferrule*[right=rec]
    { |x :: ty1, env :- e1 : ty1| \\
      |x :: forall (overline alpha) . ty1, env :- e2 : ty2|
    }
    { |env :- rec x = e1 in e2 : ty2| }

  \inferrule*[right=case]
    { |env :- e : T| \\
      |(sub C i) :: (sub ts (i,1)) -> ... -> (sub ts (i,(sub k i))) -> T `elem` env| \\
      | (sub x (i,1)) :: (sub ts (i,1)), ..., (sub x (i, sub k i)) :: (sub ts (i, sub k i)), env :- (sub e i) : ty| \\
    }
    { |env :- case e of (overline (C (overline x) -> e)) : ty| }
  \end{mathpar}

  \subsection{Type Safety}
  
  \subsubsection{Progress}
  
    If |env :- e : ty| then either |e| is a value, or there
    exists and expression |e'| and heap |H| and |H'|,
    such that |(H ; e) -> (H' ; e')|.
    
    Proof by induction on the derivation |env :- e : ty|.

  \subsubsection{Preservation}
  
    if |env :- e : ty| and |(H ; Ctx) -> (H' ; Ctx')|, then
    there exists and |env'| (with |env' # env|) such that
    |env' env :- e' : ty|.

    Proof by induction on the derivation |env :- e : ty|.
    
    Case...


\section{}

%endif


\end{document}