Properties about Compositions #
In particular, we just focus on proving that computability is close under relation composition.
def
ComputableCompositions.computable_join
{GP P₁ P₂ S₁ S₂ A₁ A₂ Err₁ Err₂ : Type}
{R₁ : GP → P₁ → S₁ → A₁ → S₁ → Prop}
{R₂ : GP → P₂ → S₂ → A₂ → S₂ → Prop}
(comp₁ :
ComputationalRel Err₁ fun (x : GP × P₁) (i : A₁) (s s' : S₁) =>
match x with
| (gp, p) => R₁ gp p s i s')
(comp₂ :
ComputationalRel Err₂ fun (x : GP × P₂) (i : A₂) (s s' : S₂) =>
match x with
| (gp, p) => R₂ gp p s i s')
:
ComputationalRel (Err₁ ⊕ Err₂) fun (x : GP × P₁ × P₂) (i : A₁ × A₂) (s s' : S₁ × S₂) =>
match x with
| (gp, p) => Products.Joint R₁ R₂ gp p s i s'
Product of computable relations are computable relations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ComputableCompositions.computable_conditional_sub
{GP P₁ S₁ A₁ A₂ Err₁ Err₂ : Type}
{R : GP → P₁ → S₁ → A₁ → S₁ → Prop}
(comp :
ComputationalRel Err₁ fun (x : GP × P₁) (i : A₁) (s s' : S₁) =>
match x with
| (gp, p) => R gp p s i s')
(lift : S₁ → A₂ → Option A₁)
(errHand : Option Err₁ → Err₂)
:
ComputationalRel Err₂ fun (x : GP × P₁) (i : A₂) (s s' : S₁) =>
match x with
| (gp, p) => InterfaceRestrictions.ConditionalSub R lift gp p s i s'
Restricting conditional actions of computable relations are computable relations.
Equations
- One or more equations did not get rendered due to their size.