Rice-Shapiro

Stream: computer science

[Matt Diamond]

Is there any interest in adding Rice-Shapiro? I have proofs of the upward and downward directions. It required adding some API for parallel evaluation of partial recursive functions (which may be useful on its own).

[Matt Diamond]

import Mathlib

open Denumerable Encodable Nat.Partrec Nat.Partrec.Code

def PFun.subfunc {α β : Type*} (f g : α →. β) : Prop :=
∀ {x y}, y ∈ f x → y ∈ g x

instance PFun.instHasSubset {α β : Type*} : HasSubset (PFun α β) := ⟨PFun.subfunc⟩

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 [f]

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_def] 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, Nat.Partrec f ∧ f.Dom.Finite ∧ f ⊆ 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 (primrec_evaln.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 f_nat_partrec : Nat.Partrec f := by rw [exists_code]; use c
  have f_mem_C : f ∈ C
  · by_contra f_notin_C
    have : f = g
    · have : ¬(mp.eval (encode c)).Dom
      · simp_rw [mp_def]
        rw [Denumerable.ofNat_encode, Part.assert_neg f_notin_C]
        exact Part.not_none_dom
      simp [hc, evaln_eq_none_of_not_halts this]
    rw [this] at f_notin_C
    contradiction
  have f_dom_finite : f.Dom.Finite
  · have mp_halts : (mp.eval (encode c)).Dom
    · simp_rw [mp_def]
      rw [Denumerable.ofNat_encode, Part.assert_pos f_mem_C]
      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_def] at this
    simp [hc, this]
  have f_sub_g : f ⊆ 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

def eval_parallel (codes : Code × Code) : ℕ →. ℕ :=
fun n => Nat.rfindOpt fun (k : ℕ) => (evaln k codes.1 n).or (evaln k codes.2 n)

lemma Computable₂.option_or {α : Type*} [Primcodable α] : Computable₂ (@Option.or α) :=
by
  let f : Option α × Option α → Option α := fun o => Option.casesOn o.1 o.2 (fun _ => o.1)
  have f_comp : Computable f
  · apply Computable.option_casesOn .fst .snd
    exact Computable.fst.comp (Computable.fst)
  apply f_comp.of_eq
  intro o
  rcases o.1.eq_none_or_eq_some with eq_none | ⟨a, eq_some⟩
  · simp [f, eq_none]
  · simp [f, eq_some]

open Primrec

lemma eval_parallel_part : Partrec₂ eval_parallel :=
Partrec.rfindOpt <|
  Computable₂.option_or.comp
    (primrec_evaln.comp (pair (pair snd (fst.comp (fst.comp fst))) (snd.comp fst))).to_comp
    (primrec_evaln.comp (pair (pair snd (snd.comp (fst.comp fst))) (snd.comp fst))).to_comp

lemma eval_parallel_some {c1 c2 : Code} {n a : ℕ} (h : eval_parallel (c1, c2) n = Part.some a)
  : a ∈ c1.eval n ∨ a ∈ c2.eval n  :=
by
  unfold eval_parallel at h
  rw [Part.eq_some_iff] at h
  have ⟨k, hk⟩ := Nat.rfindOpt_spec h
  rw [Option.mem_def, Option.or_eq_some_iff] at hk
  rcases hk with h1 | ⟨h1, h2⟩
  · left
    rw [evaln_complete]
    use k
    rw [Option.mem_def]
    exact h1
  · right
    rw [evaln_complete]
    use k
    rw [Option.mem_def]
    exact h2

lemma eval_parallel_none {c1 c2 : Code} {n : ℕ} (h : eval_parallel (c1, c2) n = Part.none)
  : c1.eval n = Part.none ∧ c2.eval n = Part.none :=
by
  unfold eval_parallel at h
  rw [Part.eq_none_iff', Nat.rfindOpt_dom] at h
  contrapose! h
  cases ne_or_eq (c1.eval n) Part.none with
  | inl hc1 =>
    rw [Part.ne_none_iff] at hc1
    obtain ⟨a, ha⟩ := hc1
    rw [Part.eq_some_iff, evaln_complete] at ha
    obtain ⟨k, hk⟩ := ha
    use k, a
    rwa [Option.or_of_isSome (Option.isSome_of_mem hk)]
  | inr hc1 =>
    have hc2 := h hc1
    rw [Part.ne_none_iff] at hc2
    obtain ⟨a, ha⟩ := hc2
    rw [Part.eq_some_iff, evaln_complete] at ha
    obtain ⟨k, hk⟩ := ha
    have evaln_c1_isNone : (evaln k c1 n).isNone = true
    · rw [Part.eq_none_iff'] at hc1
      rw [evaln_eq_none_of_not_halts hc1 k]
      rfl
    use k, a
    rwa [Option.or_of_isNone evaln_c1_isNone]

lemma eval_parallel_eq_c2_of_c1_eq_none
  (c1 c2 : Code) {n : ℕ} (hc1 : c1.eval n = Part.none)
  : eval_parallel (c1, c2) n = c2.eval n :=
by
  rcases (eval_parallel (c1, c2) n).eq_none_or_eq_some with eq_none | ⟨a, eq_some⟩
  · have ⟨h1, h2⟩ := eval_parallel_none eq_none
    rw [eq_none, h2]
  · rw [Part.eq_none_iff] at hc1
    have hc2 := (eval_parallel_some eq_some).resolve_left (hc1 _)
    rw [← Part.eq_some_iff] at hc2
    rw [eq_some, hc2]

lemma unpaired_pair {α : Type*} {f : ℕ → ℕ → α} {x y : ℕ} :
  Nat.unpaired f (Nat.pair x y) = f x y :=
by simp

theorem upward_rice_shapiro
  {C : Set (ℕ →. ℕ)} (mem_re : REPred fun c => eval c ∈ C)
  {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g)
  (f_sub_g : f ⊆ g) (fC : f ∈ C) : g ∈ C :=
by
  have g'_partrec : Nat.Partrec (Nat.unpaired (fun i n => Part.assert ((ofNat Code i).eval ∈ C) fun _ => g n))
  · rw [Partrec₂.unpaired']
    have h1 : Partrec₂ (fun i n => (Part.assert ((ofNat Code i).eval ∈ C) fun _ => Part.some ()).bind (fun _ => g n))
    · apply Partrec.bind
      apply mem_re.comp ((Computable.ofNat _).comp Computable.fst)
      exact (Partrec.nat_iff.mpr hg).comp (Computable.snd.comp .fst)
    apply h1.of_eq
    intro ⟨i, n⟩
    by_cases mem_C : (ofNat Code i).eval ∈ C
    · simp [Part.assert_pos mem_C]
    · simp [Part.assert_neg mem_C]
  have ⟨cg', cg'_eq⟩ := Code.exists_code.mp g'_partrec
  have ⟨cf, cf_eq⟩ := Code.exists_code.mp hf
  let p : Code → ℕ →. ℕ := fun c => eval_parallel (cg'.curry (encode c), cf)
  have p_partrec : Partrec₂ p
  · refine eval_parallel_part.comp ?_ Computable.snd
    exact Computable.pair
      (primrec₂_curry.comp (Primrec.const cg') (Primrec.encode.comp .fst)).to_comp
      (Computable.const cf)
  have ⟨pc, pc_eq⟩ := Code.fixed_point₂ p_partrec
  unfold p at pc_eq
  have pc_mem_C : pc.eval ∈ C
  · by_contra pc_notin_C
    have : pc.eval = f
    · funext n
      rw [pc_eq, ← cf_eq]
      apply eval_parallel_eq_c2_of_c1_eq_none
      rw [eval_curry, cg'_eq, unpaired_pair, ofNat_encode, Part.assert_neg pc_notin_C]
    rw [this] at pc_notin_C
    contradiction
  suffices pc.eval = g from this ▸ pc_mem_C
  funext n
  have cg'_eq_g : (cg'.curry (encode pc)).eval n = g n
  · rw [eval_curry, cg'_eq, unpaired_pair, ofNat_encode, Part.assert_pos pc_mem_C]
  rcases (pc.eval n).eq_none_or_eq_some with eq_none | ⟨a, eq_some⟩
  · have ⟨h1, h2⟩ := eval_parallel_none (pc_eq ▸ eq_none)
    rw [cg'_eq_g] at h1
    rw [eq_none, h1]
  · cases eval_parallel_some (pc_eq ▸ eq_some) with
    | inl h =>
      rw [← Part.eq_some_iff, cg'_eq_g] at h
      rw [eq_some, h]
    | inr h =>
      rw [cf_eq] at h
      replace h := f_sub_g h
      rw [← Part.eq_some_iff] at h
      rw [eq_some, h]

theorem rice_shapiro
  {C : Set (ℕ →. ℕ)} (h : REPred fun c => eval c ∈ C)
  {g} (hg : Nat.Partrec g)
  : g ∈ C ↔ ∃ f ∈ C, Nat.Partrec f ∧ f.Dom.Finite ∧ f ⊆ g :=
⟨
  downward_rice_shapiro h hg,
  fun ⟨_, f_mem_C, hf, _, f_sub_g⟩ =>
    upward_rice_shapiro h hf hg f_sub_g f_mem_C
⟩

[Alex Meiburg]

My impression is that Rice-Shapiro (esp. as you've formalized it above) would be much more appropriate for Mathlib than CSLib. (Super cool btw!)

[Shreyas Srinivas]

I don't see why Rice Shapiro can't be relevant to CSLib. It's not exactly undergrad material, but it is related.

[Alex Meiburg]

As in, I thought CSLib is more about providing implementations of algorithms, and proving (in an appropriate sense) things about their runtimes + memory usage... that kind of thing. I don't expect to see Computable crop much, if at all. In general, things about Turing Machines feel more mathlibby to me?

[Alex Meiburg]

I could be wrong.

[Shreyas Srinivas]

It is formalising the undergrad CS curriculum. This conventionally includes the theory of computation

[Shreyas Srinivas]

(Although if you ask Oded Goldreich, one should entirely skip this course)

[Shreyas Srinivas]

Also, as far as I can tell, the TM part of mathlib doesn't get too many new results. For computability, I think Dexter Kozen's lecture notes are a good guide to formalise things because of how detailed the treatment is (compared to Sipser's book).

[François G. Dorais]

Rice's Theorem is the canonical argument why extensional equality is not computable. Rice-Shapiro is sharper: all computable extensional information is equivalent to running a program on a finite number of inputs. This is very CS to me!

[Kim Morrison]

Yes, CSLib please! (The Turing machines perhaps only feel mathlibby for contingent historical reasons, which can be revised.)

[Martin Dvořák]

I think that neither Mathlib nor CSLib should be restricted to undergrad materials.
The line between Mathlib and CSLib, however blurry it might be, should be drawn based on the area/topic, not based on how difficult/advanced any particular result is.

[Shreyas Srinivas]

That’s not the end goal. I believe CSLib wants to first have undergrad CS as a stepping stone. How far this will work like it did for Mathlib is a different and complex question. Turing Machines are in the CS domain traditionally. Mathlib has a lot of CS-ish stuff for historical reasons. For another example the corec/stream stuff is probably best placed in batteries or core, but exists in mathlib.

[Matt Diamond]

In terms of next steps, would I just need to fork cs-lean/cslib and open a PR?

I'm also unsure about where this code would go and how to organize it

[Matt Diamond]

I'm also realizing that CSLib doesn't currently have the computability library from Mathlib which my code relies upon

[Joscha Mennicken]

cs-lean/cslib is a separate project from the CSLib this channel is about, as far as I understand. See the thread #computer science > cslib @ 💬 for a discussion on this. The two projects just share the same name, up to capitalization.

[Kim Morrison]

cs-lean/cslib depends on Mathlib, so you should just be able to import what you need.

[Matt Diamond]

@Kim Morrison is @Joscha Mennicken correct about this being a different project?

[Matt Diamond]

this is a bit confusing

[Chris Henson]

The name clash is unfortunate, and there has been discussion of changing it. I believe cs-lean/cslib was created a bit before the AWS project CSLib was publicly announced, so not intentional on anyone's part.

[Matt Diamond]

is there a link to the AWS project where I can learn more about it?

[Matt Diamond]

perhaps someone could update the channel description with more info

[Chris Henson]

I would say that cs-lean/cslib would likely welcome the contribution if it is not going to be PR'd to Mathlib. There is a computability namespace, maybe there?

[Joscha Mennicken]

Matt Diamond said:

is there a link to the AWS project where I can learn more about it?

I'm only aware of the presentation, which mentions that an initial version of Boole is supposed to be released in early August and coding kickoff is supposed to happen mid-August. I have not yet seen any website, Boole release, or git repo.

[Chris Henson]

Alex Meiburg said:

As in, I thought CSLib is more about providing implementations of algorithms, and proving (in an appropriate sense) things about their runtimes + memory usage... that kind of thing. I don't expect to see Computable crop much, if at all. In general, things about Turing Machines feel more mathlibby to me?

That presentation is believe why @Alex Meiburg said this. Hard to say for certain, but the information we have seen indicates that the results of the AWS CSLib will be very centered around this embedded language Boole and reasoning about algorithms written in it. This is why I think your Rice-Shapiro work should be in Mathlib or cs-lean/cslib.

[Matt Diamond]

ah, that makes sense... thanks for clarifying

[Fabrizio Montesi]

I think this would be great in cs-lean/cslib, as all stuff about computability would (automata, prfs, Turing machines, etc.).

We don't like the confusion either. There's an ongoing discussion on whether cslib and CSLib can be somehow merged as projects, which shouldn't take too long still. If they can't be merged, we'll figure out better names.

[Alex Meiburg]

Ah, that's indeed what had me confused... Is this channel for both?

[Matt Diamond]

now I'm curious which one Shreyas Srinivas was referring to

[Chris Henson]

Matt Diamond said:

now I'm curious which one Shreyas Srinivas was referring to

Pretty sure the AWS CSLib, as he mentioned a focus on undergrad curriculum (something mentioned in the presentation)

[Chris Henson]

Alex Meiburg said:

Ah, that's indeed what had me confused... Is this channel for both?

@Alex Meiburg This channel was created for the AWS CSLib project. cs-lean/cslib does not have a dedicated channel, but folks have been posting in the newly created computer science channel.

[Matt Diamond]

@Chris Henson perhaps the channel description could be updated to say something like "Discussion of the AWS CSLib project"

[Johan Commelin]

Done

[Johan Commelin]

@Matt Diamond would you prefer if this thread moved to #computer science ?

[Matt Diamond]

@Johan Commelin Sure, feel free to move it

[Notification Bot]

This topic was moved here from #CSLib > Rice-Shapiro by Johan Commelin.

[Thomas Waring]

i have proven rice’s theorem for the SKI calculus in a branch of cs-lean/cslib, based on @Bhavik Mehta’s presentation here https://leanprover.zulipchat.com/#narrow/stream/516743-computer-science/topic/SK.20computation/near/529713984 if that is relevant — i’m on holiday right now but i will probably pr some of that work when i’m back

[Thomas Waring]

see here https://github.com/thomaskwaring/cslib_SKI/commit/b11c41452db08d5c9fd9ad8e735de7a4d164f82a

[Thomas Waring]

A PR adding Rice's theorem for SKI is here

[Fabrizio Montesi]

Went through the PR for Rice's theorem for SKI, and it looks pretty good to me. I'd really like to get another pair of eyeballs on the theorem statement though:

https://github.com/leanprover/cslib/pull/57/files#diff-996ae1cd346aa37df0d6717ed7be2eae96473d7381004017ce54a5dd445d9668R281

@Thomas Waring some additional documentation on what the theorem is stating would be nice as well. It took me a minute to accept. :)

[Thomas Waring]

Great, thanks! the theorem statement with additional documentation now looks like this:

/--
**Rice's theorem**: no SKI term is a non-trivial predicate.

More specifically, say a term `P` is a *predicate* if, for every term `x`, `P · x` reduces to either
`TT` or `FF`. A predicate `P` is *trivial* if either it always reduces to true, or always to false.
This version of Rice's theorem derives a contradiction from the existence of a predicate `P` and the
existence of terms `x` for which `P · x` is true (`P · x ↠ TT`) and for which `P · x` is false
(`P · x ↠ FF`).
-/
theorem rice {P : SKI} (hP : ∀ x : SKI, ((P ⬝ x) ↠ TT) ∨ (P ⬝ x) ↠ FF)
    (hxt : ∃ x : SKI, (P ⬝ x) ↠ TT) (hxf : ∃ x : SKI, (P ⬝ x) ↠ FF) : False

[Fabrizio Montesi]

Much better, thanks.
@Chris Henson, @Bhavik Mehta, if any of you would like to pitch in with an LGTM (or a comment for improvement), please feel free.

[Chris Henson]

I left one style comment, but I'm not too familiar with this area to comment more deeply.