Mercurial > cpdt > repo
comparison src/Extensional.v @ 200:df289eb8ef76
Small fixes while reading student solutions
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 02 Jan 2009 08:57:25 -0500 |
| parents | 24b99e025fe8 |
| children | cbf2f74a5130 |
comparison
equal
deleted
inserted
replaced
| 199:cadeb49dc1ef | 200:df289eb8ef76 |
|---|---|
| 1011 | 1011 |
| 1012 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated. | 1012 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated. |
| 1013 | 1013 |
| 1014 It might also seem that beta reduction is a lost cause because we have no effective way of substituting in the [exp] type; we only managed to write a substitution function for the parametric [Exp] type. This is not as big of a problem as it seems. For instance, for the language we built by extending simply-typed lambda calculus with products and sums, it also appears that we need substitution for simplifying [case] expressions whose discriminees are known to be [inl] or [inr], but the function is still implementable. | 1014 It might also seem that beta reduction is a lost cause because we have no effective way of substituting in the [exp] type; we only managed to write a substitution function for the parametric [Exp] type. This is not as big of a problem as it seems. For instance, for the language we built by extending simply-typed lambda calculus with products and sums, it also appears that we need substitution for simplifying [case] expressions whose discriminees are known to be [inl] or [inr], but the function is still implementable. |
| 1015 | 1015 |
| 1016 For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr]. Also extend the correctness theorem to apply to your new definition. You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter. | 1016 For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr]. Also extend the correctness theorem to apply to your new definition. You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter. Any such axiom should only mention syntax; it should not mention any compilation or denotation functions. Following the format of the axiom from the last chapter is the safest bet to avoid proving a worthless theorem. |
| 1017 #</li># | 1017 #</li># |
| 1018 | 1018 |
| 1019 #</ol>#%\end{enumerate}% *) | 1019 #</ol>#%\end{enumerate}% *) |