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.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
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):License LogoDeutsches Urheberrecht