\documentclass[11pt]{article}

\usepackage[margin=1.45in]{geometry}
\usepackage{proof}
\usepackage{amsmath,amsthm,amssymb}
\usepackage[colorlinks=true,linkcolor=black,urlcolor=black]{hyperref}

\setlength{\inferLineSkip}{4pt}

% font{
\usepackage{pxfonts}
%% fix sans serif
\renewcommand\sfdefault{cmss}
\DeclareMathAlphabet{\mathsf}{OT1}{cmss}{m}{n}
\SetMathAlphabet{\mathsf}{bold}{OT1}{cmss}{b}{n}
% }font

\theoremstyle{definition}
\newtheorem{task}{Task}
\newtheorem{ectask}{Extra Credit Task}

\newcommand\ddd{\raisebox{0.2em}[1.3em]{$\vdots$}}
\newcommand\com{\raisebox{0.3em}{$\ ,\ \ $}}
\newcommand\hyp[2][]{\infer[#1]{#2}{}}
\newcommand\sub[3]{\infer[#2]{#3}{#1}}

\newcommand{\DD}{\mathcal{D}}
\newcommand{\EE}{\mathcal{E}}
\newcommand{\FF}{\mathcal{F}}
\newcommand{\GG}{\mathcal{G}}

\newcommand\embed[1]{\ulcorner #1 \urcorner}
\newcommand\deembed[1]{\llcorner #1 \lrcorner}

\newcommand\inl[1]{\mathsf{inl}~#1}
\newcommand\inr[1]{\mathsf{inr}~#1}
\newcommand\case[3]{\mathsf{case}(#1,#2,#3)}

\title{Constructive Logic (15-317), Fall 2012 \\
       Assignment 9: Dependent Representations}
\author{Carlo Angiuli \texttt{(cangiuli@cs)}}
\date{Out: Tuesday, November 20, 2012 \\
      Due: Thursday, November 29, 2012 (before class)}

\begin{document}
\maketitle

In this assignment, you'll explore the power of dependently-typed
programming and representations in Elf. First, you will write some short
programs over dependently-typed data structures whose invariants are
enforced by their types. Then, you'll use higher-order representations to
code up logical constructs from earlier in the semester, and you will prove
adequacy of your encoding.

The written portion of this assignment (in Section~\ref{sec:adeq}) should be typeset in
\LaTeX\ or written {\em neatly} by hand.

Your code should be submitted via AFS by copying
it to the directory \begin{verbatim}
/afs/andrew/course/15/317/submit/<userid>/hw09 
\end{verbatim} where \verb'<userid>' is replaced with your Andrew ID. Your
solutions should work in the version of Twelf installed in the course
directory.

\section{Running Twelf}

To run Twelf, execute
\begin{verbatim}
/afs/andrew/course/15/317/bin/twelf-server
\end{verbatim}
from any Andrew machine. Alternatively, you may download and install a copy
locally following the directions at \verb|http://twelf.org|, but
please test your code a final time on an Andrew machine to ensure it works
there, as that is what we will use to grade.

You can load a file \verb|foo.elf| at the prompt by typing
\begin{verbatim}
loadFile foo.elf
\end{verbatim}
To issue queries, type \verb|top| and enter predicates at the prompt.

\section{Dependent Data (15 points)}

The code in this section can be found in \verb|treelist.elf|. Consider the
following Elf definition of length-indexed lists and the corresponding
\verb|append| function:
\begin{verbatim}
nat : type.
0 : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
plus/0 : plus 0 N N.
plus/s : plus (s N) M (s P)
          <- plus N M P.

list : nat -> type.
nil : list 0.
cons : nat -> list N -> list (s N). 

append : list N -> list M -> plus N M P -> list P -> type.
%mode append +X1 +X2 +X3 -X4.
append/nil : append nil L plus/0 L.
append/cons : append (cons X L) L' (plus/s Dplus) (cons X L'')
               <- append L L' Dplus L''.
%worlds () (append _ _ _ _). 
%total L (append L _ _ _).
\end{verbatim}
%
Now suppose we have an ordinary, simply-typed representation of trees:
%
\begin{verbatim}
tree : type.
leaf : tree.
node : nat -> tree -> tree -> tree.
\end{verbatim}

Your task is to convert trees to lists, following the specification that
the resulting list's length should equal the number of elements in the
tree.

\begin{task}[5 points]
Write a predicate \verb|nelts : tree -> nat -> type.| to count the number
of elements in a tree.
\end{task}

\begin{task}[10 points]
Write a predicate \verb|flatten : {T:tree} nelts T N -> list N -> type.|
creating a list from the elements of the tree seen in depth-first order.
\end{task}

\section{Sum Types and Adequacy (25 points)}
\label{sec:adeq}

The code in this section can be found in \verb|stlc.elf|. So far, we've seen how
to encode the syntax of the simply-typed lambda calculus with a base type
\verb|o| with a single inhabitant \verb|b|:
%
\begin{eqnarray*}
\mathrm{types\;} \tau     &::=& o \mid \tau \rightarrow \tau\\
\mathrm{expressions\;} e  &::=& b \mid e\;e \mid \lambda{x{:}\tau}.e
\end{eqnarray*}
%
Suppose we add a sum (disjunction) type to the language:
%
\begin{eqnarray*}
\mathrm{types\;} \tau     &::=& o \mid \tau \rightarrow \tau \mid \tau+\tau \\
\mathrm{expressions\;} e  &::=& b \mid e\;e \mid \lambda{x{:}\tau}.e \mid
\inl e \mid \inr e \mid \case{e}{x.e}{x.e}
\end{eqnarray*}
%
Recall the inference rules for sum types:
\[
\infer[+I_1]
  {\inl e : \tau_1+\tau_2}
  {e : \tau_1}
\qquad
\infer[+I_2]
  {\inr e : \tau_1+\tau_2}
  {e : \tau_2}
\qquad
\infer[+E]
  {\case{e}{x.e_1}{y.e_2}:\tau}
  {e:\tau_1+\tau_2 &
   \deduce[\ddd]{e_1:\tau}{[x:\tau_1]} &
   \deduce[\ddd]{e_2:\tau}{[y:\tau_2]}}
\]
(NOTE: These rules are provided to help with intuition while encoding syntax;
you \emph{do not} have to encode them.)

\begin{task}[10 points]
Encode the syntax of the simply-typed lambda calculus with sum types.
\end{task}

\begin{task}[15 points]
To prove adequacy of syntax, we need an embedding function $\embed{-}$ from
first-order logic syntax to LF terms and a de-embedding function $\deembed{-}$
in the other direction that compose to the identity. Define these two functions
for your encoding.
\end{task}

\end{document}