Library OracleLanguages.ReductionTracesRelation

General definitions about reduction traces relations.

Relations between traces are represented by binary predicates.

Require Import Common.
Require Import ProgrammingLanguage.
Require Import ReductionTrace.

A relation between traces is represented by a binary predicate.

Definition trace_relation (L1 L2 : language) :=
  coplist (configuration L1) → coplist (configuration L2) → Prop.

Definition compose_trace_relations_externally
  (L1 L2 L3 : language)
  (Δ12 : trace_relation L1 L2) (Δ23 : trace_relation L2 L3)
: trace_relation L1 L3
:=
  λ tr1 tr3, ∃ tr2, Δ12 tr1 tr2 ∧ Δ23 tr2 tr3.

CoInductive gamma_correlated {L₁ L₂ : language}
            (γ : configuration L₁ → configuration L₂ → Prop)
  : coplist (configuration L₁) → coplist (configuration L₂) → Prop :=
| TerminatedCorrelated:
    ∀ c₁ c₂,
      γ c₁ c₂ →
      gamma_correlated γ (CSingle _ c₁) (CSingle _ c₂)
| StepCorrelated:
    ∀ tr₁ tr₂ n₁ n₂ tr₁' tr₂',
      γ (first tr₁) (first tr₂) →
      skipn n₁ tr₁ = Some tr₁' →
      skipn n₂ tr₂ = Some tr₂' →
      n₁ + n₂ > 0 →
      gamma_correlated γ tr₁' tr₂' →
      gamma_correlated γ tr₁ tr₂.