feat(untyped): define CBN and Standard evaluation strategies

[m-ow]

This is the first step towards the Standardization Theorem.

Instead of the classic (and painful) Barendregt approach, I defined Standard reduction
relying on CBN to find the head redex, which makes the proofs much nicer.

[lengyijun]

Hi, I am doing something similar.
I have verified eta-postpone theorem yet.

I also have verified leftmost theorem in debruijn index.

We are working on https://github.com/awesome-lambda-calculus/Fokker_challenge , normalization theorem is of most importance to us.

[m-ow]

Hi! Really cool project!
You mentioned using De Bruijn indices, but I'm writing the Standardization theorem in Locally Nameless.
Are you planning to open a PR to add the De Bruijn representation? Let's coordinate our efforts to avoid duplicating work.

[m-ow]

Just read through your docs and I'm glad to see the project officially uses Locally Nameless.
I also noticed that you are currently blocked by the Standardization theorem. I can focus my efforts there so your team can use it soon. Let me know what you think and how you'd like to proceed!

[lengyijun]

https://github.com/awesome-lambda-calculus/Fokker_challenge/issues/3

[chenson2018]

Looks straightforward, just a couple of small golfs:

[chenson2018]

I think for the other reduction strategies we namespace all these lemmas. Especially since you do so for Standard.lc_refl below this feels odd.

[m-ow]

Thanks for the review!

[chenson2018]

Looks good, thanks!

[lengyijun]

@chenson2018 Why merge such unfinished code?

[chenson2018]

@chenson2018 Why merge such unfinished code?

We in general encourage making small PRs. This seemed fine to me for an initial pass at adding these definitions.

[lengyijun]

@m-ow May I ask what project you are working on that requires this definition?
For fokker_challenge, this definition of standard theorem looks useless.

In my development of fokker_challenge, changes to cslib are saved in enhancedcslib/ directory for several weeks, until I can make sure this is useful and general enough to contribute to upstream.

[chenson2018]

this definition of standard theorem looks useless.

Instead of phrasing things so negatively, could you please explain the specific issue that you have with the definitions in this PR?

[lengyijun]

Personally I prefer https://www.is.c.titech.ac.jp/~kashima/pub/C-145.pdf

Actually I have verified most part of the paper, but I am still testing them in fokker_challenge, so I will not pr soon.

I don't understand merge such a pr in one day.

[lengyijun]

this definition of standard theorem looks useless.

Instead of phrasing things so negatively, could you please explain the specific issue that you have with the definitions in this PR?

I doubt this is helpful to verify "two vars are not enough".
I am currently still experimenting with various definitions.
I don't understand why the decision is being made so quickly.

https://github.com/awesome-lambda-calculus/Fokker_challenge/wiki/Two-vars-are-not-enough

[lengyijun]

BTW: "Formalization in Coq of the Standardization Theorem for λ-calculus" is not based on locallynameless

[chenson2018]

BTW: "Formalization in Coq of the Standardization Theorem for λ-calculus" is not based on locallynameless

It seems unlikely to be relevant that this reference is not specifically using locally nameless binding, as most theorems we care about are independent of this?

So I don't understand merge such a pr in one day.

I've still not understood your specific objection to these definitions. They seemed very straightforward to me, so I merged the PR. There is no rush, but if you follow up with a specific alternative proposal and a fleshed out explanation of why it works better, I will certainly consider it.

[lengyijun]

In this pr, standardization is parallel style.
In https://www.is.c.titech.ac.jp/~kashima/pub/C-145.pdf, standardization is small step style.

Proof in parallel style might be easier to write.

@m-ow @chenson2018

[lengyijun]

Actually I have the whole proof this pr, but it is not tested in fokker_challenge, so I didn't push a pr:

3176a427-5996-4dfd-85d5-33b8f32eff1a-aristotle.tar.gz

[m-ow]

@lengyijun Thanks for the feedback.
I'd like to clarify a couple of points regarding the definitions in this PR:

In this pr, standardization is parallel style.

The proof strategy in this PR is not parallel, it's CBN based (following Calisto, adapted to locally nameless).

I doubt this is helpful to verify "two vars are not enough".

Agreed that the current PR is not sufficient for fokker_challenge on its own. The next step is M ⭢ₛ N ↔ M ↠βᶠ N, followed by the leftmost reduction theorem. These are the next PRs I have in mind.

[lengyijun]

@m-ow Are you going to define properties of Normal FullBeta ?

[m-ow]

If you already have Normal and related properties in locally nameless, I'd encourage you to open a PR for them. Let's avoid overlap

[lengyijun]

@m-ow I will not pr those. Thanks for your work. I will focus on following theorems, although I don't have any idea now:

theorem betaeta_factor_betaNF {M N : Term} (h : StepsBetaEta M N) (hN : NormalFormBetaEta N) :
    ∃ P, StepsBeta M P ∧ NormalFormBeta P ∧ StepsEta P N := by

lemma sn_eta_step [DecidableEq Var] [HasFresh Var]
  (t_st_t' : t ⭢ηᶠ t') (sn_t : SN FullBeta t) : SN FullBeta t'