Prove that a SKI expression does not terminate

Stream: new members

[Patrick Johnson]

Trying to find the best way to prove that a SKI expression does not terminate using induction. We say that an expression terminates iff it evaluates to some unique irreducible constant Z in a finite number of steps.

Expression S I I (S I I) reduces to itself, so it cannot possibly terminate. But in order to prove that, we seem to be forced to use natural numbers or function iterator eval^[n]. Can we somehow prove it directly using only induction on term type?

import tactic.induction

namespace test

inductive expr : Type
| Z : expr
| K : expr
| S : expr
| app : expr → expr → expr
open expr

infix ` ~ `:100 := app
def I := S ~ K ~ K

def eval : expr → expr
| (K ~ a ~ b) := a
| (S ~ a ~ b ~ c) := a ~ c ~ (b ~ c)
| (a ~ b) := eval a ~ b
| a := a

inductive term : expr → Prop
| mk₀ : term Z
| mk₁ {e : expr} : term (eval e) → term e

example : ¬term (S ~ I ~ I ~ (S ~ I ~ I)) :=
begin
  intro h,
  induction' h,
  sorry
end

end test

[Mario Carneiro]

Based on some example evaluations, I do not see "S I I (S I I) reduces to itself". It looks more like it reduces to S I I (I ... (I (S I I)))

[Patrick Johnson]

Right, I was not precise enough. Fixed.

[Mario Carneiro]

Having a theorem of the form term (eval^[n] e) -> term e will certainly be helpful since each evaluation involves many steps before reaching something useful

[Patrick Johnson]

Yeah, it is easy to prove, but I would like to avoid it if possible:

lemma term_iff_iter_eval {e : expr} :
  term e ↔ ∃ (n : ℕ), (eval^[n]) e = Z :=
begin
  split; intro h,
  { induction' h,
    { use 0, refl },
    { cases ih with n ih, use n + 1, exact ih }},
  { cases h with n h, induction' n,
    { cases h, exact term.mk₀ },
    { apply term.mk₁, apply ih, exact h}},
end

lemma term_of_term_iter_eval {e : expr} {n : ℕ}
  (h : term (eval^[n] e)) : term e :=
begin
  induction' n,
  { exact h },
  { apply term.mk₁, apply ih, exact h },
end

[Mario Carneiro]

you need to think about the induction hypothesis here. Many other terms appear in the evaluation

[Mario Carneiro]

def bad : ℕ → expr
| 0 := S ~ I ~ I
| (n+1) := I ~ bad n

example (m n) : eval^[2] (bad (m+1) ~ bad n) = bad m ~ bad n := rfl
example (n) : eval^[3] (bad 0 ~ bad n) = bad n ~ bad (n+1) := rfl

theorem aux (m n) : ¬term (bad m ~ bad n) := sorry
example : ¬term (S ~ I ~ I ~ (S ~ I ~ I)) := aux 0 0

[Mario Carneiro]

def bad : ℕ → expr
| 0 := S ~ I ~ I
| (n+1) := I ~ bad n

inductive is_bad : expr → Prop
| base (m n) : is_bad (bad m ~ bad n)
| K (a m n) : is_bad (K ~ bad m ~ a ~ bad n)

theorem is_bad_not_term (e) : is_bad e → ¬ term e :=
begin
  intros h1 h2,
  induction h2 with e h1 ih; cases h1,
  case base : m n { cases m,
    { exact ih (is_bad.base (n+1) (n+1)) },
    { exact ih (is_bad.K _ m n) } },
  case K : a m n { exact ih (is_bad.base m n) },
end

example : ¬term (S ~ I ~ I ~ (S ~ I ~ I)) := is_bad_not_term _ (is_bad.base 0 0)

[Patrick Johnson]

That's an interesting approach. I was hoping we can somehow avoid introducing natural numbers and/or new datatypes, but seems I'm out of luck. This was my proof:

inductive has_Z : expr → Prop
| mk₀ : has_Z Z
| mk₁ {a b} : has_Z a → has_Z (a ~ b)
| mk₂ {a b} : has_Z b → has_Z (a ~ b)

lemma has_Z_of_has_Z_eval {e : expr} (h : has_Z (eval e)) : has_Z e :=
begin
  induction' e, repeat { exact h },
  cases e with a d, repeat { cases' h, cases h, apply has_Z.mk₂ h }, exact h,
  cases a with a c, cases' h, exact has_Z.mk₀.mk₂.mk₁,
  exact h.mk₁.mk₂.mk₁, exact h.mk₂.mk₂.mk₁,
  repeat { exact h }, cases a with a b;
  try { cases' h, exact (ih_e h).mk₁, exact has_Z.mk₂ h },
  cases' h; cases' h; try { exact h.mk₂ }, exact h.mk₂.mk₁.mk₁, exact h.mk₂.mk₁,
end

lemma has_Z_of_term {e : expr} (h : term e) : has_Z e :=
by { induction' h, exact has_Z.mk₀, exact has_Z_of_has_Z_eval ih }

example : ¬term (S ~ I ~ I ~ (S ~ I ~ I)) :=
by { intro h, replace h := has_Z_of_term h, repeat { cases' h }}

[Mario Carneiro]

Well, this only proves that the term doesn't have a Z in it; it wouldn't work in general for proving nontermination (in the sense of reaching a term which is a fixed point of eval).

[Mario Carneiro]

The basic structure of the proof here is to give an explicit characterization of a set of terms which is closed under the eval function and for which none of them are Z or normal forms or whatever

[Mario Carneiro]

There aren't any new datatypes introduced, but nat is used in the definition of bad, is that what you mean? You can define bad inductively if you prefer but I think this gives the cleanest proof

[Mario Carneiro]

inductive bad : expr → Prop
| zero : bad (S ~ I ~ I)
| succ {a} : bad a → bad (I ~ a)

inductive is_bad : expr → Prop
| base {m n} : bad m → bad n → is_bad (m ~ n)
| K {a m n} : bad m → bad n → is_bad (K ~ m ~ a ~ n)

theorem is_bad_not_term (e) : is_bad e → ¬ term e :=
begin
  intros h1 h2,
  induction h2 with e h1 ih; cases h1,
  case base : m n hm hn { cases hm with m hm',
    { exact ih (is_bad.base hn.succ hn.succ) },
    { exact ih (is_bad.K hm' hn) } },
  case K : a m n hm hn { exact ih (is_bad.base hm hn) },
end

example : ¬term (S ~ I ~ I ~ (S ~ I ~ I)) := is_bad_not_term _ (is_bad.base bad.zero bad.zero)

[Mario Carneiro]

Here's a version of your proof using no_Z instead of is_bad

inductive no_Z : expr → Prop
| K : no_Z K
| S : no_Z S
| app {a b} : no_Z a → no_Z b → no_Z (a ~ b)

theorem no_Z_not_term (e) : no_Z e → ¬ term e :=
begin
  intros h1 h2,
  induction h2 with e h1' ih, cases h1 with a z ha hz,
  apply ih, clear ih h1', have := h1,
  induction this with a z ha hz iha; try { exact h1 },
  cases ha with a y ha' hy; try { exact h1 },
  cases ha' with a x ha'' hx; try { exact h1 }, { exact hy },
  cases ha'' with a x ha''' hx; try { exact h1 },
  { exact hx.app hz },
  { exact (hx.app hz).app (hy.app hz) },
  { exact (iha ha).app hz },
end

theorem no_Z.I : no_Z I := (no_Z.S.app no_Z.K).app no_Z.K
theorem no_Z.SII : no_Z (S ~ I ~ I) := (no_Z.S.app no_Z.I).app no_Z.I
example : ¬term (S ~ I ~ I ~ (S ~ I ~ I)) := no_Z_not_term _ (no_Z.SII.app no_Z.SII)