Mercurial > cpdt > repo

comparison src/ProgLang.v @ 464:e53d051681b0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish complete proofreading pass
author Adam Chlipala <adam@chlipala.net>
date Wed, 29 Aug 2012 17:17:17 -0400
parents 92f386c33e94
children 4320c1a967c2
comparison
equal deleted inserted replaced
463:218361342cd2 464:e53d051681b0
328 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran 328 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran
329 329
330 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2. 330 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2.
331 ]] 331 ]]
332 332
333 However, Coq rejects this definition for failing to meet the %\index{strict positivity restriction}%strict positivity restriction. For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining. Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic. 333 However, Coq rejects this definition for failing to meet the %\index{strict positivity requirement}%strict positivity restriction. For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining. Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic.
334 334
335 An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq. Here the idea is to parametrize the syntax type by a type family standing for a _representation of variables_. *) 335 An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq. Here the idea is to parametrize the syntax type by a type family standing for a _representation of variables_. *)
336 336
337 Section var. 337 Section var.
338 Variable var : type -> Type. 338 Variable var : type -> Type.