search

jaccokrijnen / plutus-cert

0 stars 2 forks source link

Simplify definition of contextual equivalence? #54

Open jaccokrijnen opened 4 months ago

jaccokrijnen commented 4 months ago

Could we simplify

Definition contextually_approximate
  (e e' : Term) Δ Γ T
  :=
  (Δ ,, Γ |-+ e  : T) /\
  (Δ ,, Γ |-+ e' : T) /\
  forall (C : Context),
    ([] ,, [] |-C C : (Δ ,, Γ ▷ T) ↝ Ty_Unit) ->
    forall (v : Term),
      context_apply C e ==> v ->
      exists v',
        context_apply C e' ==> v' /\
        (v = v' \/ (is_error v /\ is_error v')).

into

Definition contextually_approximate
  (e e' : Term) Δ Γ T
  :=
  (Δ ,, Γ |-+ e  : T) /\
  (Δ ,, Γ |-+ e' : T) /\
  forall (C : Context),
    ([] ,, [] |-C C : (Δ ,, Γ ▷ T) ↝ Ty_Unit) ->
    forall (v : Term),
      context_apply C e ==> Unit ->
      context_apply C e' ==> Unit
.

When making the bi-implication (contextually_equivalent), this should imply the other version: if either C[e] terminates with an error, the other will also terminate with an error (when t has type unit, and $t \Downarrow v$, then v can only be unit constant or an error).

If this is the case, we don't have to worry about removing type annotation on errors (https://github.com/jaccokrijnen/plutus-cert/issues/53).