528c4b4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Note on metatheory

528c4b4Edwin Brady14 years ago

papers/impl-paper/elaboration.tex+5−1

compare with master

unifiedsplit

@@ -586,6 +586,10 @@ the goal type.

586

587\FFIG{

588\begin{array}{lll}

589+\mbox{\textbf{Tactic}} & \mbox{\textbf{Resulting Proof Term}} &

590+\mbox{\textbf{Queue}}

591+\medskip

592+\\

589\mbox{Initial state}

593\mbox{Initial state}

590& \hole{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vx

594& \hole{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vx

591& \langle\vx\rangle \\

595& \langle\vx\rangle \\

@@ -701,7 +705,7 @@ the goal type.

701Figure \ref{mkidrefine} shows how each step of this sequence of tactics affects

705Figure \ref{mkidrefine} shows how each step of this sequence of tactics affects

702the proof state and hole queue. In each step, the underlined fragment of the

706the proof state and hole queue. In each step, the underlined fragment of the

703term is the fragment in focus. One might observe that the

707term is the fragment in focus. One might observe that the

704−$\MO{Attack}$/$\MO{Solve}$ pairs may be unnecessary in this case, as the term

708+$\MO{Attack}$/$\MO{Solve}$ pairs are unnecessary in this case, as the term

705is already in a form suitable for introduction. However, we retain these for

709is already in a form suitable for introduction. However, we retain these for

706uniform treatment of introductions.

710uniform treatment of introductions.

707

711

papers/impl-paper/typechecking.tex+35

@@ -243,6 +243,7 @@ be implemented in the usual way~\cite{loh2010tutorial}.

243{Cumulativity}

244{cumul}

245

246+

246\subsection{Inductive Families}

247\subsection{Inductive Families}

247

248

248\label{sect:inductivefams}

249\label{sect:inductivefams}

@@ -472,6 +473,40 @@ trees~\cite{Augustsson1985}.

472% In practice, for efficiency, pattern matching is implemented by compiling the match clauses to

473% In practice, for efficiency, pattern matching is implemented by compiling the match clauses to

473% a tree of case expressions~\cite{Augustsson1985}.

474% a tree of case expressions~\cite{Augustsson1985}.

474

475

476+\subsection{Metatheory}

477+

478+\FFIG{

479+\AR{

480+\mbox{\textbf{TODO}}\\

481+\mbox{Church-Rosser}

482+\\

483+\mbox{Subject Reduction}

484+\\

485+\mbox{Strengthening}

486+\\

487+\mbox{Cut}

488+\\

489+}

490+}

491+{Metatheoretic properties of \TT{}}

492+{metatheory}

493+

494+\TT{} respects the usual metatheoretic properties, as shown in Figure

495+\ref{metatheory}. Specifically: the \demph{Church-Rosser} property

496+(i.e. that distinct reduction sequences lead to the same normal form);

497+\demph{subject

498+reduction} (i.e. that computation preserves type); the \demph{cut} property

499+(i.e. that $\RW{let}$-bound terms may be substituted into their scope); and

500+\demph{strengthening} (i.e. that introducing new definitions into scope does

501+not affect typechecking).

502+

503+One property which is noticeably absent is \demph{strong normalisation}.

504+Although desirable to preserve termination and decidability of type checking,

505+we allow diverging terms for pragmatic reasons as \Idris{} is primarily a

506+programming language rather than a theorem prover. Nevertheless, we do

507+\emph{check} for totality in order to be sure which terms are safe to

508+evaluate at compile time.

509+

475\subsection{Totality checking}

510\subsection{Totality checking}

476

511

477In order to ensure termination of type checking we must distinguish terms for

512In order to ensure termination of type checking we must distinguish terms for