Closures of may and must convergence for contextual equivalence
We show on an abstract level that contextual equivalence in non-deterministic program calculi defined by may- and must-convergence is maximal in the following sense. Using also all the test predicates generated by the Boolean, forall- and existential closure of may- and must-convergence does not change the contextual equivalence. The situation is different if may- and total must-convergence is used, where an expression totally must-converges if all reductions are finite and terminate with a value: There is an infinite sequence of test-predicates generated by the Boolean, forall- and existential closure of may- and total must-convergence, which also leads to an infinite sequence of different contextual equalities.
| Author: | Manfred Schmidt-Schauß, David Sabel |
|---|---|
| URN: | urn:nbn:de:hebis:30-61000 |
| Series (Serial Number) | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (35) |
| Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
| Place of publication: | Frankfurt [am Main] |
| Document Type: | Working Paper |
| Language: | English |
| Date of Publication (online): | 29.01.2009 |
| Year of first Publication: | 2008 |
| Publishing Institution: | Univ.-Bibliothek Frankfurt am Main |
| Tag: | Programmkalküle ; Programmkorrektheit formal semantics ; program correctness; programming calculi |
| SWD-Keyword: | Formale Semantik |
| HeBIS PPN: | 209490411 |
| Institutes: | Informatik |
| Dewey Decimal Classification: | 004 Datenverarbeitung; Informatik |
| MSC-Classification: | 68Q55 Semantics [See also 03B70, 06B35, 18C50] |
| Sammlungen: | Universitätspublikationen |
| Licence (German): |  Veröffentlichungsvertrag für Publikationen ohne Print on Demand |
