Computability under a semantic promise

An effective presentation is sometimes most naturally described by a raw, computably encoded type of programs together with a semantic validity promise. For example, a raw partial-recursive program is a valid decider when it halts on every input. Validity need not itself be decidable: the algorithm is required to halt only when its code satisfies the promise.

ComputableOnPromise valid eval says that eval is one uniform partial-recursive evaluator and is total on every valid code. DecidesOnPromise additionally says that its Boolean result decides a relation on the promised inputs. ComputablePredOnPromise valid p existentially packages such an evaluator for a unary predicate.

These predicates deliberately retain the raw Primcodable code type. Replacing it by the subtype {c // valid c} would incorrectly require a computable encoding of a generally undecidable semantic property.

def ComputableOnPromise {Code Input Output : Type} [Primcodable Code] [Primcodable Input] [Primcodable Output] (valid : Code → Prop) (eval : Code → Input →. Output) : Prop

A uniform partial-recursive evaluator which is guaranteed to return on every input whenever its raw code satisfies valid. No effectiveness assumption is made about the semantic promise itself.

Equations

• ComputableOnPromise valid eval = (Partrec₂ eval ∧ ∀ (c : Code), valid c → ∀ (x : Input), (eval c x).Dom)

def DecidesOnPromise {Code Input : Type} [Primcodable Code] [Primcodable Input] (valid : Code → Prop) (eval : Code → Input →. Bool) (relation : Code → Input → Prop) : Prop

A uniform partial-recursive Boolean evaluator which, on valid codes, always returns and returns true exactly when relation c x holds.

Equations

• DecidesOnPromise valid eval relation = (ComputableOnPromise valid eval ∧ ∀ (c : Code), valid c → ∀ (x : Input), relation c x ↔ true ∈ eval c x)

def ComputablePredOnPromise {Code : Type} [Primcodable Code] (valid predicate : Code → Prop) : Prop

A predicate is computable on the promised inputs when one partial-recursive Boolean evaluator is total and correct at every input satisfying valid.

Unlike ComputablePred, the evaluator may diverge away from the promise. This is essential for semantic promises such as "this program halts on every word": the raw program syntax is effectively encoded even though validity itself is undecidable.

Equations

• ComputablePredOnPromise valid predicate = ∃ (eval : Code →. Bool), Partrec eval ∧ ∀ (c : Code), valid c → (eval c).Dom ∧ (predicate c ↔ true ∈ eval c)

theorem ComputablePredOnPromise.ofComputablePred {Code : Type} [Primcodable Code] {valid predicate : Code → Prop} (h : ComputablePred predicate) : ComputablePredOnPromise valid predicate

An ordinary computable predicate is computable under any promise.

theorem ComputablePredOnPromise.toComputablePred {Code : Type} [Primcodable Code] {valid predicate : Code → Prop} (h : ComputablePredOnPromise valid predicate) (hall : ∀ (c : Code), valid c) : ComputablePred predicate

If every input satisfies the promise, promise computability is ordinary ComputablePred computability.

theorem computablePredOnPromise_true_iff {Code : Type} [Primcodable Code] (predicate : Code → Prop) : ComputablePredOnPromise (fun (x : Code) => True) predicate ↔ ComputablePred predicate

With the trivial promise, ComputablePredOnPromise is exactly ComputablePred.

theorem Partrec.true_mem_re {Code : Type} [Primcodable Code] {eval : Code →. Bool} (heval : Partrec eval) : REPred fun (c : Code) => true ∈ eval c

Acceptance by a partial-recursive Boolean evaluator is recursively enumerable: run the evaluator, return when it says true, and diverge when it says false.

theorem DecidesOnPromise.total {Code Input : Type} [Primcodable Code] [Primcodable Input] {valid : Code → Prop} {eval : Code → Input →. Bool} {relation : Code → Input → Prop} (h : DecidesOnPromise valid eval relation) {c : Code} (hc : valid c) (x : Input) : (eval c x).Dom

The totality component available from a promise decider.

theorem DecidesOnPromise.correct {Code Input : Type} [Primcodable Code] [Primcodable Input] {valid : Code → Prop} {eval : Code → Input →. Bool} {relation : Code → Input → Prop} (h : DecidesOnPromise valid eval relation) {c : Code} (hc : valid c) (x : Input) : relation c x ↔ true ∈ eval c x

The correctness component available from a promise decider.