feat(untyped): the Leftmost Reduction Theorem

[m-ow]

Introduces leftmost reduction ⭢ℓ, a beta-step contracting the redex at position 0, together with normal forms, and proves the Leftmost Reduction Theorem: if a term beta-reduces to a normal form, the leftmost strategy reaches it too.
The result falls out of standardization, following Copes (2018).

Builds on top of #679

[lengyijun]

Can you add 2 theorems :

1. NormalForm M <-> Normal FullBeta M
2. Decidable Normal FullBeta

[m-ow]

@lengyijun Sounds good, I'll get both into a separate PR soon :)

[lengyijun]

Should we rename Normal to NormalBeta ?
Or put it in namespace "FullBeta"

Normal may also refer to Normal FullBetaEta or Normal FullEta

[lengyijun]

@m-ow Hi, what's your plan after this pr

[m-ow]

Honestly, no fixed plan yet, but your project sounds really interesting. Feel free to point me at what's the priority on your side, happy to take a look!

[lengyijun]

We will formalize "2 vars are not enough" after this pr is merged.

There will still be 1400 cases unprocessed. I haven't even studied them at all.

You can randomly pick a few and research them.

I will also pr my fork step by step.
Perhaps you can help me optimize the proof.

[chenson2018]

@m-ow Before I review for more detailed changes, I think I'm missing some high-level points about the defintions (some of which I maybe should have asked in earlier PRs, sorry!).

BetaAt seems to clearly align with the literature, but I think I'm missing where the connection to the usual definition of standard reduction is happening. I am expecting to somewhere see that if we have BetaAt A B x and BetaAt B C y with x <= y this is a standard reduction and that this is equivalent to Standard. Am I missing where this appears in a different form or otherwise misunderstanding something? (I'm following along with https://www.is.c.titech.ac.jp/~kashima/pub/C-145.pdf that's mentioned in your reference)

[m-ow]

You're right, it's not there. The results here only rely on the inductive Standard relation, both sources I followed actually keep the sequence definition as a separate development. It's clearly worth having though, sorry for the gap! If you think it's best, I'll open a new PR to add the sequence definition and its equivalence with Standard.

[chenson2018]

Yeah, it is pretty standard to use some equivalent inductive that's easier to work with (I assume this is why we have Standard not directly written in terms of BetaAt?), but I think we should have this proof of equivalence to make sure the definition corresponds to what we want informally.

Maybe because these are so closely related they should just go in the same module? Feel free to move things around as needed.

[m-ow]

I've added the equivalence! Feel free to take another look whenever it suits you :)

[lengyijun]

Is it possible to prove

BetaAt M P i -> BetaAt M Q i -> P = Q

[m-ow]

Sure, added.

[m-ow]

Is it possible to prove

Yes, I'll add it! Probably together with BetaNormal M ↔ Normal FullBeta M​ in the next PR

[chenson2018]

A few more questions/comments about the definitions added:

[chenson2018]

What do you think about combining these like

Suggested change

	| appNoAbsL : BetaAt M M' i → ¬IsAbs M → BetaAt (app M N) (app M' N) i
	/-- Reducing an abstraction operator advances the position by one. -/
	| appAbsL : BetaAt M M' i → IsAbs M → BetaAt (app M N) (app M' N) (i + 1)
	| appL : BetaAt M M' i → BetaAt (app M N) (app M' N) (i + if IsAbs M then 1 else 0)

and similarly for the right? (Either adding a Decidable instance for IsAbs or making it boolean-valued)

[m-ow]

Good idea, did it. Went with Decidable IsAbs over boolean

[chenson2018]

Marking as unresolved in light of the dependent elimination issue discussed below. I do still like it, I think we just need an additional induction principle.

[chenson2018]

I think it would be more intuitive for this to follow Relation.ReflTransGen and have the contructors be refl and tail (not just switching the naming, but the side you build the reduction on) and have StandardSeq.head as an additional theorem/induction principle.

[m-ow]

Addressed. StandardSeq now follows ReflTransGen, with refl, tail, and a derived head theorem

[chenson2018]

How do you feel about the ergonomics of this change, since this now carries a lower bound as well? Do you think it is a useful addition?

[lengyijun]

/-- Values are irreducible terms. -/
inductive Value : Term Var → Prop
| abs (e : Term Var) : e.abs.LC → e.abs.Value

/-- `IsAbs m` holds when `m` is an abstraction. -/
@[scoped grind]
inductive IsAbs : Term Var → Prop
| abs (m : Term Var) : IsAbs (abs m)

instance (m : Term Var) : Decidable (IsAbs m) := by
  cases m
  case abs => exact isTrue (.abs _)
  all_goals exact isFalse (by intro _; contradiction)

Why put in lcat.lean ? Unrelated, strange.

[chenson2018]

Why put in lcat.lean ? Unrelated, strange.

I very briefly explained why I asked for this above, but to be more explicit:

• having both Value and IsAbs seems redundant, or at least one should be defined in terms of the other
• I didn't want to prompt that unrelated refactor in this PR, so asked for them to be placed next to each other as a reminder of this
• In terms of dependencies, this is the highest spot in the imports where that is possible

Edit: and lastly while you could place IsAbs on its own in the Basic.lean module, as a practical matter we almost always need to import LC anyway.

[lengyijun]

I know, the position of Value is quite strange before this pr.
I really like the elegance of lcat.lean.
I don't like anything strange here.
I just really surprised that lcat need re-compiled after git pull

[chenson2018]

I know, the position of Value is quite strange before this pr.

I don't understand the reasoning here. It makes sense for this definition to occur as soon as local closure is available. A single definition like this is not a detriment to the structure of the module.

(Let's maybe table this discussion for later, it's gotten a bit off topic for this PR)

[lengyijun]

@m-ow Could you please group the theorems ?

awesome-lambda-calculus@ab40e9d

[lengyijun]

My more aggressive opinion is to separate countredex to a new file.
Because personally I don't care anything about standard reduction.

BTW StandardReduction.lean is the largest file in untyped lambda calculus now.
Worth splitting up

[lengyijun]

Can you add theorm of fv

#[grind]
lemma step_fv (step : BetaAt i M N) : N.fv ⊆ M.fv := by

[lengyijun]

Can you rebase on main?
Toolchain has updated.

[m-ow]

@lengyijun Addressed everything except the free-variable theorem, which I'll handle in a follow-up PR to keep this diff smaller

[lengyijun]

@m-ow @chenson2018 Unable to cases t.abs ⭢ℓ t'

theorem foo {t t': Term String}
(step : t.abs ⭢ℓ t') : exists a, t' = a.abs := by
  cases step with
  | appR _ => sorry  -- error here
  | abs xs _ => sorry

Expected: fall into the abs case, derive t' must be Term.abs

[chenson2018]

@m-ow @chenson2018 Unable to cases t.abs ⭢ℓ t'

theorem foo {t t': Term String}
(step : t.abs ⭢ℓ t') : exists a, t' = a.abs := by
  cases step with
  | appR _ => sorry  -- error here
  | abs xs _ => sorry

Expected: fall into the abs case, derive t' must be Term.abs

Yes, with the typing of BetaAt now, this is not surprising. We should have an induction principle that matches the original set of constructors that @m-ow wrote to avoid the dependent typing.

[lengyijun]

@m-ow Can you group the theorems ?

awesome-lambda-calculus@f015ac3

[lengyijun]

@m-ow @chenson2018 Unable to cases t.abs ⭢ℓ t'

theorem foo {t t': Term String}
(step : t.abs ⭢ℓ t') : exists a, t' = a.abs := by
  cases step with
  | appR _ => sorry  -- error here
  | abs xs _ => sorry

Expected: fall into the abs case, derive t' must be Term.abs

Yes, with the typing of BetaAt now, this is not surprising. We should have an induction principle that matches the original set of constructors that @m-ow wrote to avoid the dependent typing.

Thx, I got it. I should generalize 0 to variable

[lengyijun]

Leftmost.normalization (lc : LC M) 

LC M is redundant

[lengyijun]

Can you add 2 theorems :

1. Relation.Normalizable FullBeta M <-> Relation.Normalizable Leftmost M
2. Relation.Normal FullBeta M <-> Relation.Normal Leftmost M

[lengyijun]

Can you add this theorem as well :

omit [HasFresh Var] in
lemma BetaAt.lc_l (h : BetaAt i M M') (lc : LC M') : LC M := by
  induction h with
  | outer lc_M lc_N => grind
  | appL _ ih =>
    cases lc with
    | app lc_L lc_R => exact .app (ih lc_L) lc_R
  | appR _ ih =>
    cases lc with
    | app lc_L lc_R => exact .app lc_L (ih lc_R)
  | abs xs _ ih =>
    cases lc with
    | abs ys _ h_body =>
      apply LC.abs (xs ∪ ys)
      intro z hz
      exact ih z (by grind) (h_body z (by grind))

[lengyijun]

@m-ow Lc is redundant :

| outer : LC (abs M) → LC N → BetaAt 0 (app (abs M) N) (M ^ N)
| outer : BetaAt 0 (app (abs M) N) (M ^ N)