comparison src/ProgLang.v @ 465:4320c1a967c2

Spell check
author Adam Chlipala <adam@chlipala.net>
date Wed, 29 Aug 2012 18:26:26 -0400
parents e53d051681b0
children 6252dd4540a9
comparison
equal deleted inserted replaced
464:e53d051681b0 465:4320c1a967c2
80 (** Now we have some choices as to how we represent the syntax of programs. The two sections of the chapter explore two such choices, demonstrating the effect the choice has on proof complexity. *) 80 (** Now we have some choices as to how we represent the syntax of programs. The two sections of the chapter explore two such choices, demonstrating the effect the choice has on proof complexity. *)
81 81
82 82
83 (** * Dependent de Bruijn Indices *) 83 (** * Dependent de Bruijn Indices *)
84 84
85 (** The first encoding is one we met first in Chapter 9, the _dependent de Bruijn index_ encoding. We represent program syntax terms in a type familiy parametrized by a list of types, representing the _typing context_, or information on which free variables are in scope and what their types are. Variables are represented in a way isomorphic to the natural numbers, where number 0 represents the first element in the context, number 1 the second element, and so on. Actually, instead of numbers, we use the [member] dependent type family from Chapter 9. *) 85 (** The first encoding is one we met first in Chapter 9, the _dependent de Bruijn index_ encoding. We represent program syntax terms in a type family parameterized by a list of types, representing the _typing context_, or information on which free variables are in scope and what their types are. Variables are represented in a way isomorphic to the natural numbers, where number 0 represents the first element in the context, number 1 the second element, and so on. Actually, instead of numbers, we use the [member] dependent type family from Chapter 9. *)
86 86
87 Module FirstOrder. 87 Module FirstOrder.
88 88
89 (** Here is the definition of the [term] type, including variables, constants, addition, function abstraction and application, and let binding of local variables. *) 89 (** Here is the definition of the [term] type, including variables, constants, addition, function abstraction and application, and let binding of local variables. *)
90 90
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 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. 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 parameterize 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.
339 339
340 Inductive term : type -> Type := 340 Inductive term : type -> Type :=
430 (** %\vspace{-.15in}%[[ 430 (** %\vspace{-.15in}%[[
431 = "(((fun x => (fun x' => (x + x'))) N) N)" 431 = "(((fun x => (fun x' => (x + x'))) N) N)"
432 ]] 432 ]]
433 *) 433 *)
434 434
435 (** However, it is not necessary to convert to first-order form to support many common operations on terms. For instance, we can implement substitution of one term in another. The key insight here is to _tag variables with terms_, so that, on encountering a variable, we can simply replace it by the term in its tag. We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute. During recursion, new variables are added, but they are only tagged with their own term equivalents. Note that this function [squash] is parametrized over a specific [var] choice. *) 435 (** However, it is not necessary to convert to first-order form to support many common operations on terms. For instance, we can implement substitution of one term in another. The key insight here is to _tag variables with terms_, so that, on encountering a variable, we can simply replace it by the term in its tag. We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute. During recursion, new variables are added, but they are only tagged with their own term equivalents. Note that this function [squash] is parameterized over a specific [var] choice. *)
436 436
437 Fixpoint squash var t (e : term (term var) t) : term var t := 437 Fixpoint squash var t (e : term (term var) t) : term var t :=
438 match e with 438 match e with
439 | Var _ e1 => e1 439 | Var _ e1 => e1
440 440
657 657
658 (** We can state a well-formedness condition for closed terms: for any two choices of tag type families, the parallel instantiations belong to the [wf] relation, starting from an empty variable isomorphism. *) 658 (** We can state a well-formedness condition for closed terms: for any two choices of tag type families, the parallel instantiations belong to the [wf] relation, starting from an empty variable isomorphism. *)
659 659
660 Definition Wf t (E : Term t) := forall var1 var2, wf nil (E var1) (E var2). 660 Definition Wf t (E : Term t) := forall var1 var2, wf nil (E var1) (E var2).
661 661
662 (** After digesting the syntactic details of [Wf], it is probably not hard to see that reasonable term encodings will satsify it. For example: *) 662 (** After digesting the syntactic details of [Wf], it is probably not hard to see that reasonable term encodings will satisfy it. For example: *)
663 663
664 Theorem three_the_hard_way_Wf : Wf three_the_hard_way. 664 Theorem three_the_hard_way_Wf : Wf three_the_hard_way.
665 red; intros; repeat match goal with 665 red; intros; repeat match goal with
666 | [ |- wf _ _ _ ] => constructor; intros 666 | [ |- wf _ _ _ ] => constructor; intros
667 end; intuition. 667 end; intuition.