Semantics encoding: Difference between revisions

Revision as of 11:43, 20 April 2005

Revision as of 11:44, 20 April 2005

Line 50:

This assumes the existence of a notion of observation on both language A and language B. In programming languages, typical observables are results of inputs and outputs, by opposition to pure computation. In a description languages such as [[HTML]], a typical observable is the result of page rendering.

; soundness : for every observable <math>obs_A</math> on terms of A, there isexists an observable <math>obs_B</math> of terms of B such that for any term <math>T_A</math> with observable <math>obs_A</math>, <math>[T_A]</math> has observable <math>obs_B</math>.

; completeness : for every observable <math>obs_A</math> on terms of A, there isexists an observable <math>obs_B</math> on terms of B such that for any term <math>[T_A]</math> with observable <math>obs_B</math>, <math>T_A</math> has observable <math>obs_A</math>.

=== Preservation of simulations ===