From a425fa840fdd390b69cfca68a9a7698a6583bdab Mon Sep 17 00:00:00 2001 From: ben Date: Wed, 16 Mar 2016 06:15:20 -0400 Subject: [PATCH] [icfp] a pretty section 2 --- icfp-2016/solution.scrbl | 55 ++++++++++++++++++++-------------------- icfp-2016/texstyle.tex | 2 +- 2 files changed, 28 insertions(+), 29 deletions(-) diff --git a/icfp-2016/solution.scrbl b/icfp-2016/solution.scrbl index c4e24bc..7beb272 100644 --- a/icfp-2016/solution.scrbl +++ b/icfp-2016/solution.scrbl @@ -24,21 +24,22 @@ Using @exact|{\RktMeta{expr}}| to denote the set of syntactically valid, symboli @exact|{$$\interp\ : \big\{\RktMeta{expr} \rightarrow ({\RktVal{val}} \cup {\tt \RktVal{\#false}})\big\}$$}| -If @exact|{${\tt p?} \in \interp$}| and @exact|{${\tt e} \in \emph{expr}$}|, +If @exact|{\RktMeta{p?} $\in \interp$}| and @exact|{\RktMeta{e} $\in \RktMeta{expr}$}|, it may be useful to think of - @exact|{${\tt (p?~e)}$}| as @emph{evidence} that the expression @exact|{${\tt e}$}| - is recognized by @exact|{${\tt p?}$}|. -Alternatively, @exact|{${\tt (p?~e)}$}| is a kind of interpolant@~cite[c-jsl-1997], - representing key data embedded in @exact|{${\tt e}$}|. -Correct interpretation functions @exact|{${\tt p?}$}| obey two guidelines: + @exact|{\RktMeta{(p? e)}}| as @emph{evidence} that the expression @exact|{\RktMeta{e}}| + is recognized by @exact|{\RktMeta{p?}}|. +Alternatively, @exact|{\RktMeta{(p? e)}}| is a kind of interpolant@~cite[c-jsl-1997], + representing data embedded in @exact|{\RktMeta{e}}| that justifies a certain + program transformation. +Correct interpretation functions @exact|{\RktMeta{p?}}| obey two guidelines: @itemize[ @item{ - The expressions for which @exact|{${\tt p?}$}| returns a non-@racket[#false] + The expressions for which @exact|{\RktMeta{p?}}| returns a non-@racket[#false] value must have some common structure. } @item{ - Non-@racket[#false] results @exact|{${\tt (p?~e)}$}| are computed by a + Non-@racket[#false] results @exact|{\RktMeta{(p? e)}}| are computed by a uniform algorithm and must have some common structure. } ] @@ -51,50 +52,48 @@ Functions in the set @exact|{$\elab$}| of @emph{elaborations} map expressions to expressions, for instance replacing a call to @racket[curry] with a call to @racket[curry_3]. We write elaboration functions as @exact{$\elabf$} and their application - to an expression @exact{$e$} as @exact{$\llbracket e \rrbracket$}. + to an expression @exact|{\RktMeta{e}}| as @exact|{$\llbracket$\RktMeta{e}$\rrbracket$}|. Elaborations are allowed to fail raising syntax errors, which we notate as @exact|{$\bot$}|. @exact|{$$\elab : \big\{ {\RktMeta{expr}} \rightarrow ({\RktMeta{expr}} \cup \bot)\big\} $$}| The correctness specification for an elaborator @exact{$\elabf \in \elab$} - is defined in terms of the language's typing judgment @exact|{$~\vdash {\tt e} : \tau$}| - and evaluation relation @exact|{$\untyped{{\tt e}} \Downarrow {\tt v}$}|. -The notation @exact|{$\untyped{{\tt e}}$}| is the untyped erasure of @exact|{${\tt e}$}|. + is defined in terms of the language's typing judgment @exact|{$~\vdash \RktMeta{e} : \tau$}| + and evaluation relation @exact|{$\untyped{\RktMeta{e}} \Downarrow \RktVal{v}$}|. +The notation @exact|{$\untyped{\RktMeta{e}}$}| is the untyped erasure + of @exact|{\RktMeta{e}}|. We also assume a subtyping relation @exact|{$\subt$}| on types. -Let @exact|{$\elabfe{{\tt e}} = {\tt e'}$}|: +Let @exact|{$\elabfe{\RktMeta{e}} = \RktMeta{e'}$}|: @itemlist[ @item{@emph{ - If @exact|{$~\vdash {\tt e} : \tau$}| and @exact|{$~\vdash {\tt e'} : \tau'$}| + If @exact|{$~\vdash \RktMeta{e} : \tau$}| and @exact|{$~\vdash \RktMeta{e'} : \tau'$}| @exact|{\\}| then @exact|{$\tau' \subt \tau$}| @exact|{\\}| and both - @exact|{$\untyped{{\tt e}} \Downarrow {\tt v}$}| and - @exact|{$\untyped{{\tt e'}} \Downarrow {\tt v}$}|. + @exact|{$\untyped{\RktMeta{e}} \Downarrow \RktVal{v}$}| and + @exact|{$\untyped{\RktMeta{e'}} \Downarrow \RktVal{v}$}|. }} - @; e:t e':t' => t' <: t /\ e <=> e' @item{@emph{ - If @exact|{$~\not\vdash {\tt e} : \tau$}| but @exact|{$~\vdash {\tt e'} : \tau'$}| + If @exact|{$~\not\vdash \RktMeta{e} : \tau$}| but @exact|{$~\vdash \RktMeta{e'} : \tau'$}| @exact|{\\}| - then @exact|{$\untyped{{\tt e}} \Downarrow {\tt v}$}| and - @exact|{$\untyped{{\tt e'}} \Downarrow {\tt v}$}|. + then @exact|{$\untyped{\RktMeta{e}} \Downarrow \RktVal{v}$}| and + @exact|{$\untyped{\RktMeta{e'}} \Downarrow \RktVal{v}$}|. }} - @; -e:t e':t' => e <=> e' @item{@emph{ - If @exact|{$~\vdash {\tt e} : \tau$}| but @exact|{${\tt e'} = \bot$}| - or @exact|{$~\not\vdash {\tt e'} : \tau'$}| + If @exact|{$~\vdash \RktMeta{e} : \tau$}| but @exact|{$\RktMeta{e'} = \bot$}| + or @exact|{$~\not\vdash \RktMeta{e'} : \tau'$}| @exact|{\\}| - then @exact|{$\untyped{{\tt e}} \Downarrow \mathsf{wrong}$}| or - @exact|{$\untyped{{\tt e}}$}| diverges. + then @exact|{$\untyped{\RktMeta{e}} \Downarrow \RktMeta{wrong}$}| or + @exact|{$\untyped{\RktMeta{e}}$}| diverges. }} - @; e:t -e':t' => e^ ] -If neither @exact|{${\tt e}$}| nor @exact|{${\tt e'}$}| type checks, then we have no guarantees +If neither @exact|{\RktMeta{e}}| nor @exact|{\RktMeta{e'}}| type checks, then we have no guarantees about the run-time behavior of either term. In a perfect world both would diverge, but the fundamental limitations of static typing@~cite[fagan-dissertation-1992] and computability @@ -119,6 +118,6 @@ Our implementation uses a tagging protocol, and this lets us share information between unrelated elaboration function in a bottom-up recursive style. The same protocol helps us implement binding forms: when interpreting a variable, we check for an associated tag. -Formally speaking, this either changes the codomain of functions in @exact{$\elab$} +Formally speaking, this changes either the codomain of functions in @exact{$\elab$} or introduces an elaboration environment mapping expressions to values. diff --git a/icfp-2016/texstyle.tex b/icfp-2016/texstyle.tex index 420e116..bfbf0c5 100644 --- a/icfp-2016/texstyle.tex +++ b/icfp-2016/texstyle.tex @@ -32,7 +32,7 @@ \usepackage{amssymb} \newcommand{\interp}{\mathcal{I}} -\newcommand{\untyped}[1]{\hat{#1}} +\newcommand{\untyped}[1]{{\,#1}_\flat} \newcommand{\trans}{\mathcal{T}} \newcommand{\elab}{\mathcal{E}} \newcommand{\elabfe}[1]{\llbracket #1 \rrbracket}