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ßORCiDGND, David SabelORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30-61000 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank35maymust.pdf |
Parent Title (English): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 35 |
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 |
Year of Completion: | 2008 |
Year of first Publication: | 2008 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2009/01/29 |
Tag: | Programmkalküle; Programmkorrektheit formal semantics; program correctness; programming calculi |
GND Keyword: | Formale Semantik |
Issue: | 12 |
First Page: | 12 |
Last Page: | 1 |
HeBIS-PPN: | 209490411 |
Institutes: | Informatik und Mathematik / Informatik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
MSC-Classification: | 68-XX COMPUTER SCIENCE (For papers involving machine computations and programs in a specific mathematical area, see Section {04 in that areag 68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) / 68Qxx Theory of computing / 68Q55 Semantics [See also 03B70, 06B35, 18C50] |
Licence (German): | Deutsches Urheberrecht |