Adequate Models for Recursive Program Schemes
Submitted by mernst on Wed, 2011-11-30 14:35
| Title | Adequate Models for Recursive Program Schemes |
| Publication Type | Thesis |
| Year of Publication | 1989 |
| Authors | Ernst MD |
| Date or Month Published | June |
| University | MIT Department of Electrical Engineering and Computer Science |
| City | Cambridge, MA |
| Thesis Type | mastersBachelors thesis |
| Abstract | <p>This thesis is a pedagogical exposition of adequacy for recursive program schemes in the monotone frame. Adequacy relates the operational and denotational meanings of a term; it states that for any term of base type, the operational and denotational meanings are identical. Adequacy is typically proved in the continuous frame. This is a pedagogically questionable step; in order to prove adequacy (or some other property) of a pair of semantics, it would be desirable to show the property directly, without introducing superfluous notions. This difficulty is particularly acute because, in general, not all monotone functions are continuous. </p> <p> This thesis attempts to work out the concept of adequacy for a class of monotone first-order recursive program schemes, using Vuillemin and Manna's method of ``safe'' computation rules. The attempt is very nearly successful, but at a crucial point the fact that the scheme-definable functions are, in fact, continuous as well as monotone must be used.</p> |
| Citation Key | Ernst89 |
Last changed Mon, 2013-06-03 10:27

cs.