Commit 78c18db5 authored by Adam Chlipala's avatar Adam Chlipala

First draft of full prose for GeneralRec

parent 7057f379
......@@ -267,3 +267,22 @@
publisher = "MIT Press",
chapter = "8"
}
@article{Capretta,
author = {Venanzio Capretta},
title = {General Recursion via Coinductive Types},
journal = {Logical Methods in Computer Science},
volume = 1,
number = 2,
year = 2005,
pages = {1--18},
}
@inproceedings{Megacz,
author = {Adam Megacz},
title = {A coinductive monad for prop-bounded recursion},
booktitle = {Proceedings of the {ACM} Workshop Programming
Languages meets Program Verification},
pages = {11--20},
year = {2007},
}
This diff is collapsed.
......@@ -465,7 +465,7 @@ Error: variable n should be bound to a term.
>> *)
Abort.
(** What is going wrong here? The answer has to do with the dual status of Ltac as both a purely functional and an imperative programming language. The basic programming language is purely functional, but tactic scripts are one %``%#"#datatype#"#%''% that can be returned by such programs, and Coq will run such a script using an imperative semantics that mutates proof states. Readers familiar with %\index{monads}\index{Haskell}%monadic programming in Haskell%~\cite{monads,IO}% may recognize a similarity. Side-effecting Haskell programs can be thought of as pure programs that return %\emph{%#<i>#the code of programs in an imperative language#</i>#%}%, where some out-of-band mechanism takes responsibility for running these derived programs. In this way, Haskell remains pure, while supporting usual input-output side effects and more. Ltac uses the same basic mechanism, but in a dynamically typed setting. Here the embedded imperative language includes all the tactics we have been applying so far.
(** What is going wrong here? The answer has to do with the dual status of Ltac as both a purely functional and an imperative programming language. The basic programming language is purely functional, but tactic scripts are one %``%#"#datatype#"#%''% that can be returned by such programs, and Coq will run such a script using an imperative semantics that mutates proof states. Readers familiar with %\index{monad}\index{Haskell}%monadic programming in Haskell%~\cite{monads,IO}% may recognize a similarity. Side-effecting Haskell programs can be thought of as pure programs that return %\emph{%#<i>#the code of programs in an imperative language#</i>#%}%, where some out-of-band mechanism takes responsibility for running these derived programs. In this way, Haskell remains pure, while supporting usual input-output side effects and more. Ltac uses the same basic mechanism, but in a dynamically typed setting. Here the embedded imperative language includes all the tactics we have been applying so far.
Even basic [idtac] is an embedded imperative program, so we may not automatically mix it with purely functional code. In fact, a semicolon operator alone marks a span of Ltac code as an embedded tactic script. This makes some amount of sense, since pure functional languages have no need for sequencing: since they lack side effects, there is no reason to run an expression and then just throw away its value and move on to another expression.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment