Library OracleLanguages.DifferenceLanguage


General definitions for difference languages.
In this module, we introduce basic definitions about difference languages for deterministic programming languages.
A difference language between two deterministic languages L1 and L2 is a record of type difference_language L1 L2 made of a syntax for differences and an interpretation function.
While the syntax for differences is left as abstract as possible, the semantics of differences uses a fixed (but general) interpretation domain : the relations between reduction traces.
A difference term δ written in a difference_language L1 L2 is an sound difference between P1 and P2 if its interpretation relates the reduction traces of P1 and P2.

Require Import ProgrammingLanguage.
Require Import ReductionTrace.
Require Import ReductionTracesRelation.

A difference language is defined by a syntax for differences and a semantic that interprets differences as relations between configurations.
Record difference_language (L1 L2 : language) : Type :=
{
  
The type for the terms of the difference language.
  difference : Type;

  
The interpretation function.
  interpret : difference → trace_relation L1 L2;
}.


A difference δ is a sound difference between S and T, if the interpretation of δ relates the trace of S and the trace of T.
Definition sound_program_difference (L1 L2 : language) (D : difference_language L1 L2)
 (δ : difference D) (pL1 : prog L1) (pL2 : prog L2) : Prop :=
  interpret D δ (program_trace L1 pL1) (program_trace L2 pL2).