Any interest in adding Rice-Shapiro?

Stream: mathlib4

[Matt Diamond]

I wrote up a Lean proof for Rice-Shapiro the other day and was wondering if I should use this as an opportunity to contribute to Mathlib. Would that theorem make sense for the Computability module?

[Johan Commelin]

@Matt Diamond Sorry for the slow response. There isn't much activity in that corner of mathlib.
Is your formalization available somewhere? Can you say a bit about how it went? Any tough spots, or was it mostly smooth sailing?

[Matt Diamond]

Sorry for the even slower response! The proof I wrote up needed to be cleaned up a bit, but I ended up losing interest in the project and then eventually I lost the proofs themselves (I'm not the most organized person :sweat_smile:). However, I recently took another swing at the downward half of Rice-Shapiro, and while I'm still not sure if I'm going to finish the rest of the proof (I don't believe anyone needs it at this point, and I'm just a hobbyist) I figure I might as well post it here in case someone else is curious or wants to finish it themselves.

Rice-Shapiro is a statement about sets of partial recursive functions with a recursively enumerable membership predicate. It states that a function $g$ is a member of such a set if and only if the set contains a finite subfunction of $g$. It captures the idea that a recursively enumerable predicate can only check a finite number of values before halting, so any function that passes the membership test must have done so on the basis of only a finite subset of its graph.

(Rice-Shapiro is a generalization of Rice's theorem, which we have as docs#ComputablePred.rice.)

The proof I'm posting here is the forward direction of the iff: if $g$ is a member of the set, then there exists an $f$ in the set which is a finite subfunction of $g$. The reverse direction (if $f$ is in the set and $f$ is a subfunction of $g$, then $g$ is in the set) isn't too difficult... the proof that I know of requires the formalization of parallel execution of partial recursive functions, but this can be done very simply using Nat.rfindOpt, Code.evaln, and the OrElse operator (<|>).

The proof of the forward direction is kind of funny. We define the desired function $f$ with the following logic:

• $f(x)$ runs the r.e. membership predicate on itself, but using the bounded (and therefore decidable) evaln function, with the bound set to $x$
• if the predicate halts, then loop forever (return Part.none)
• otherwise, return $g(x)$

This simple setup gives us everything we need:

• $f$ must be a member of the set, because if it isn't, the membership predicate will never halt and the function will always return $g(x)$, in which case $f = g$, but that would mean $g$ isn't a member of the set, which contradicts our initial assumption.
• $f$ must have a finite domain, because at some point the input (which bounds evaln) will be high enough to allow the membership predicate to halt, and the function will return Part.none for all values beyond that threshold.
• $f$ is clearly a subfunction of $g$, as the only values it can take are Part.none and $g(x)$.

Anyway, here's the proof:

import Mathlib

open Denumerable Encodable Nat.Partrec Nat.Partrec.Code

def PFun.subfunc (f g : ℕ →. ℕ) : Prop :=
∀ x y, y ∈ f x → y ∈ g x

lemma Computable.option_isSome {α} [Primcodable α] : Computable (@Option.isSome α) :=
by
  let f : Option α → Bool := fun o => Option.casesOn o false (fun _ => true)
  have : Computable f := Computable.option_casesOn .id (.const false) (.const true)
  apply this.of_eq
  intro n
  cases n <;> simp

lemma evaln_eq_none_of_not_halts
  {c : Code} {n} (h : ¬(c.eval n).Dom)
  : ∀ k, c.evaln k n = Option.none :=
by
  contrapose! h
  simp_rw [Option.ne_none_iff_exists] at h
  rcases h with ⟨k, x, hx⟩
  rw [eq_comm, ← Option.mem_iff] at hx
  rw [Part.dom_iff_mem]
  use x
  exact evaln_sound hx

lemma exists_evaln_of_halts
  {c : Code} {n} (h : (c.eval n).Dom)
  : ∃ k x, x ∈ c.evaln k n :=
by
  have : (c.eval n).get h ∈ c.eval n := Part.get_mem _
  rw [evaln_complete] at this
  rcases this with ⟨k, hk⟩
  use k, (c.eval n).get h

theorem downward_rice_shapiro
  (C : Set (ℕ →. ℕ)) (h : RePred fun c => eval c ∈ C)
  {g} (hg : Nat.Partrec g) (gC : g ∈ C)
  : ∃ f ∈ C, f.Dom.Finite ∧ f.subfunc g :=
by
  have mem_pred_part : Nat.Partrec (fun n => Part.assert ((ofNat Code n).eval ∈ C) fun _ => 0) := Partrec.nat_iff.mp h
  let ⟨mp, mp_def⟩ := exists_code.1 mem_pred_part
  let f' : Code → ℕ →. ℕ := fun c x => bif (Code.evaln x mp (encode c)).isSome then Part.none else g x
  have partrec_f' : Partrec₂ f' :=
    Partrec.cond
      (Computable.option_isSome.comp (evaln_prim.comp (.pair (.pair .snd (.const mp)) (Primrec.encode.comp .fst))).to_comp)
      Partrec.none
      ((Partrec.nat_iff.2 hg).comp .snd)
  obtain ⟨c, hc⟩ := fixed_point₂ partrec_f'
  unfold f' at hc
  set f := c.eval
  have h1 : f ∈ C
  · by_contra h
    have : f = g
    · have : ¬(mp.eval (encode c)).Dom
      · simp_rw [mp_def]
        rw [Denumerable.ofNat_encode, Part.assert_neg h]
        exact Part.not_none_dom
      simp [hc, evaln_eq_none_of_not_halts this]
    rw [this] at h
    contradiction
  have h2 : f.Dom.Finite
  · have mp_halts : (mp.eval (encode c)).Dom
    · simp_rw [mp_def]
      rw [Denumerable.ofNat_encode, Part.assert_pos h1]
      trivial
    obtain ⟨k, x, hk⟩ := exists_evaln_of_halts mp_halts
    rw [Set.finite_iff_bddAbove, bddAbove_def]
    use k
    intro j hj
    contrapose! hj
    have := evaln_mono hj.le hk
    rw [Option.mem_iff] at this
    simp [hc, this]
  have h3 : f.subfunc g
  · intro x y hxy
    cases (evaln x mp (encode c)).isSome.eq_false_or_eq_true with
    | inl eq_true => simp [hc, eq_true] at hxy
    | inr eq_false => simpa [hc, eq_false] using hxy
  use f

[Bjørn Kjos-Hanssen]

There's a Rice's Theorem in docs#Halting already. Maybe your result can be shown to generalize that?

[Matt Diamond]

Not sure... that's a separate theorem regarding computable predicates, whereas my understanding is that Rice-Shapiro is a distinct theorem about recursively enumerable predicates.

[Matt Diamond]

They're certainly related, and Rice-Shapiro does generalize Rice in the sense that it goes from computable to r.e.

I'll add a note to the post above!

[Bjørn Kjos-Hanssen]

I am thinking that if we consider the empty function g, we get Rice's Theorem as a corollary of Rice-Shapiro: if g is in the set then the set is everything, and otherwise the complement is everything.

[Matt Diamond]

interesting... so we would show that the only computable predicate on partial functions is the predicate that doesn't check anything, and this predicate lets the empty function through, so therefore it lets all functions through by Rice-Shapiro?

[Matt Diamond]

that could work

[Matt Diamond]

well, maybe I'm misunderstanding, because once you've shown that the always true or false predicate is the only computable one, then it seems like you're already at the finish line

[Bjørn Kjos-Hanssen]

The sketch of proof I have in mind is:
Assume S is a both r.e. and co-r.e. index set. Consider the empty function g.
By excluded middle, either g is in S or g is in the complement of S.
In the former case, S = Nat, by Rice-Shapiro.
In the latter case, complement-of-S = Nat, by Rice Shapiro.
Therefore, Rice's Theorem has been proved.

[Matt Diamond]

oh, I see... right, because Rice-Shapiro applies not just to membership but also non-membership if it's r.e. and co-r.e.

Edit: Here's a proof of Rice using Upward Rice-Shapiro:

import Mathlib

open Nat.Partrec.Code

def PFun.subfunc (f g : ℕ →. ℕ) : Prop :=
∀ x y, y ∈ f x → y ∈ g x

theorem upward_rice_shapiro
  {C : Set (ℕ →. ℕ)} (h : RePred fun c => eval c ∈ C)
  {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g)
  (hfg : f.subfunc g) (f_mem : f ∈ C) : g ∈ C := sorry

def empty : ℕ →. ℕ := fun _ => Part.none

lemma empty_subfunc {g : ℕ →. ℕ} : empty.subfunc g :=
fun _ => by simp [empty]

theorem rice
  {C : Set (ℕ →. ℕ)} (h : ComputablePred fun c => eval c ∈ C)
  {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g)
  (f_mem : f ∈ C) : g ∈ C :=
(em (empty ∈ C)).elim
  (upward_rice_shapiro h.to_re Nat.Partrec.none hg empty_subfunc)
  fun empty_not_mem =>
    have f_mem_compl : f ∈ Cᶜ := upward_rice_shapiro h.not.to_re Nat.Partrec.none hf empty_subfunc empty_not_mem
    (f_mem_compl f_mem).elim