Strong norm for Stlc

Stream: CSLib

[David Wegmann]

I am trying to formalize strong normalization for lambda calculus right now, I found the Acc type, is there an inverse of this type, so that Acc R t holds if there are now infinite seqences t R x R y ... ?

I know I can just write (Acc (Function.swap FullBeta) t), but is there something nicer?

[Chris Henson]

I don't recommend doing it directly with accessibility, but if you go that route, you will notice we define Relation.Terminating similarly, just using docs#WellFounded instead of directly using Acc. I don't believe there is a more primitive inverse like you are looking for.

Usually however when proving strong normalization, you will see it characterized inductively as

import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta

open Cslib.LambdaCalculus.LocallyNameless.Untyped
open scoped Term

inductive SN {α} : Term α → Prop
| sn {t} : (∀ t', (t ⭢βᶠ t') → SN t') → SN t

and you can prove that this is equivalent to the various ways of saying there are no infinite reductions. Again the locally nameless piece is a little harder to find references for, but these ideas are the same regardless of binding.

[David Wegmann]

Thank you!

[David Wegmann]

I am pretty much done with the saturated sets, now I need multisubstitutions for the soundness lemma. Is there something like this already in the library? I can only see a map that substitutes a single variable, but it seems to connect to some other part of the library.

[David Wegmann]

I can hack something together, I am just asking because I want to of course reuse everything available as much as possible

[Chris Henson]

No, there is no definition of multiple substitution. I am somewhat surprised you need it, but I guess that depends on exactly the proof structure. Is your work so far in a branch I could look at?

[David Wegmann]

Not jet, I did not push anything yet, because it is still messy:

I can quickly summarize the type of proof structure I am familiar with:

You write a semantic map that maps each type to a subset of strongly normalizing terms, and these sets are closed under some types of terms and operations.

Then you prove soundness like this:
image.png
in this definition of soundness, \sigma is a substitition, that contains finitely many variables and terms to replace them with.

[David Wegmann]

the way I always implemented this is by having a list that recursively substitutes with the ordinary subst map, but if there is something nicer I'd use that of course.

[David Wegmann]

If you know/prefer a specific proof structure that avoids this, please link me a document with the proof, then I will try to formalize that instead.

[David Wegmann]

def multisubst (M : Term Var) (σ : List (Var × Term Var)) : Term Var :=
  match σ with
  | [] => M
  | ⟨ x, s ⟩ :: σ' => M.subst x (multisubst s σ')

def satisfies_term (σ : List (Var × Term Var)) (t : Term Var) (τ : Ty Base) :=
  t ∈ semanticMap τ → (multisubst t σ) ∈ semanticMap τ

def satisfies_context (σ : List (Var × Term Var)) (Γ : Context Var (Ty Base)) :=
  ∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multisubst (Term.fvar x) σ) ∈ semanticMap τ

def consequence {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} :=
  ∀ σ, (satisfies_context σ Γ) → satisfies_term σ t τ

This works, I just wonder if there is something nicer/wether you like it

[Chris Henson]

Oh sorry, you are right that it is needed. I would probably not recurse on the context like that, it seems easier if it is structural on the term since you just need to replace free variables?

[David Wegmann]

I am not recursing on the context, the strong norm proof will essentially recurse over the typing derivation and push variables onto some accumulated \sigma. other parts of the proof will use that substitution again.

But I need to build up a list of variables and terms for that somewhere.

[Chris Henson]

When you said multiple substitution, I imagined something like

import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
import Cslib.Languages.LambdaCalculus.LocallyNameless.Context

namespace Cslib.LambdaCalculus.LocallyNameless.Untyped

variable [DecidableEq Var]

def Term.multisubst (Γ : Context Var (Term Var)) : Term Var → Term Var
| bvar i => bvar i
| fvar x => Γ.dlookup x |>.getD (fvar x)
| app t₁ t₂ => app (multisubst Γ t₁) (multisubst Γ t₂)
| abs t => abs (multisubst Γ t)

[Chris Henson]

They are free variables, so we can do this all at once, right?

[Chris Henson]

(Also a small tip: try to never write .subst directly, always use the notation)

[David Wegmann]

I think so.

The lecture notes I am familiar with actually defines substiution over a map that maps variables to terms, and then that map replaces all variables with whatever it maps to, the variables not to be replaced are just mapped to itself.

This is quite elegant but requires careful management of tracking wether a variable is free or not.

We could replace "subst" with that type of substitution and then still implement the HasSubstitution typeclass with a map that only has a support of a single variable. that way it wouldn't break anything and I think it would work well with the locally nameless stuff because then you essentially just have free variables connected to that operation.

[Chris Henson]

I would need to see concretely what you're proposing and that it doesn't break anything in STLC or System F. My guess is it will be delicate interacting with the locally nameless binding, but I am happy to consider a PR proving me wrong!

We are planning to additionally support something like this style of substitution, closely following Autosubst, but this is a longer term project because of the metaprogramming involved.

[David Wegmann]

At the moment I'll only try to produce a single file strongnorm.lean :)

Did you consider nominal techniques for variable management?

[Chris Henson]

By "nominal" , do you mean in the sense of Nominal Isabelle?

[David Wegmann]

well lean doesn't have nominal stuff built in the type theory, so no, I mean by formalizing nominal sets and then formalizing all stuff that uses variables using nominal sets. I do not know if this is a practical idea though.

[Chris Henson]

The direction I am headed is to define a command elaborator that looks like a usual inductive type, but is tagged with information about where binding occurs and has multiple options for what "backend" is used for binding. I think it is evident from prior work that this works for locally nameless and scoped indices (with the substitution you described earlier). It might be possible to have a nominal sets backend in this framework, but I have no immediate plan to do so. (This is all very early in development, so details are subject to change!)

[Bhavik Mehta]

I think formalising nominal sets would be cool, but I agree that something closer to Autosubst would be more practical for handling bindings and variables in practice

[David Wegmann]

did autosubst manage to include dependent types yet? Last I heard you could do pretty much everything in like 70 lines for System F or stuff like that but once you add dependent types it just doesn't work.

[David Wegmann]

but last time I did type theory was a few years ago.

[David Wegmann]

@Chris Henson progress report on STLC strong norm:

The main structure soundness lemma stands and has no sorries, there are some trivial lemmas left, like wen app t s is SN then just t is SN, but the main issue that i still need to resolve is a single variable management issue. Not sure how long that will take, if I am lucky tonight, but I can't promise anything.

[David Wegmann]

Is there some lemma that says something like

if x is not free in t
then t[x:=s] = t?

[Chris Henson]

I think you want Untyped.Term.subst_fresh

[David Wegmann]

thanks!

[Chris Henson]

No problem. And in general, good to hear you're making progress!

[David Wegmann]

I think I mostly resolved all variable management issues arising from the locally nameless approach.

There are 7 sorries left for the entire proof, most of them are stuff like

when t.app s is strongly normalizing, then so is just t. I am working on that right now.

[David Wegmann]

I made a lot more progress, but I am still stuck with some of the locally nameless things

[Chris Henson]

Maybe you could open a draft PR if it is pretty close otherwise? That would make it easier for me to take a look at the last few sorry.

[David Wegmann]

https://github.com/leanprover/cslib/pull/327
@Chris Henson

[David Wegmann]

I did open the pull request. Just a disclaimer, I have not contributed on a larger project before, so I still have to get used to style guides and all that stuff for pull requests, this is just very messy code. I planned to eliminate all the sorries before I wanted to submit anything at all.

I think I identified the main issue. Even the untyped terms require to be locally closed for reductions. I have to make some adjustments to incorperate this in a few of the substition/strong_norm lemmas.

[Chris Henson]

Yeah, in your lemmas about operations preserving SN and also in semanticMap, you need to carry around a hypothesis/conjunction that the term is locally closed. But at a quick glance it looks like it's headed in the tight direction.

Totally fine that there is work to be done style wise at this point, we want to be friendly to new contributors. I've marked it as a draft to indicate this. I will hold off on style remarks until you get these last sorry ironed out. Please ping me if you need any help.

[David Wegmann]

I think I'll manage, I just took a lot longer to figure out some caviats of the locally nameless approach. But the intuition how general the lemmas have to be seems to carry over from pure DeBrujin.

[IntGrah]

Chipping in to say hi

[IntGrah]

have de bruijn levels been considered instead of locally nameless syntax?

[IntGrah]

also, intrinsic well scopedness too
so bvar : Fin n -> Term n

[Chris Henson]

Yes, these will appear in a future PR that I am working on already.

[David Wegmann]

@IntGrah Thanks for contributing app_sn btw!

[David Wegmann]

I think I figured out the crucial requirement for the proof to work, one needs to demand that saturated sets only contain Locally closed terms. A single sorry remains in the Stlc/StrongNorm.lean file.

Suppose M ^ N is locally closed. Does this imply that M.abs is locally closed? It feels true but I haven't yet found a lemma for that.

[Sehun Kim]

Could you update your repository?

[David Wegmann]

one second

[David Wegmann]

I pushed it to my fork: https://github.com/leanprover/cslib/compare/main...WegmannDavid:cslib:main

[Chris Henson]

@David Wegmann That lemma seems plausible to me as well. The non-abstraction cases at least are easy.

I think you are still missing some locally closed hypothesis in your semanticMap. I would expect the definition to be something like:

def semanticMap (τ : Ty Base) : Set (Term Var) :=
  match τ with
  | Ty.base _ => { t : Term Var | SN t ∧ LC t }
  | Ty.arrow τ₁ τ₂ => { t | ∀ s, (LC s ∧ s ∈ semanticMap τ₁) → t.app s ∈ semanticMap τ₂ }

which I think will resolve the last sorry in that file.

[David Wegmann]

that LC hypothesis for s won't be necessary. It is obtained by the induction hypothesis. we are proving that semanticMap τ is saturated by induction on τ. in the case of the arrow type, we must show that

semanticMap (τ₁ -> τ₂) is saturated while already assuming that semantic map τ₁ and semanticMap τ₂. all elements inside saturated sets are locally closed, so s will be too.

[David Wegmann]

also the arrow case already doesn't contain any sorries. its the base case that containes the sorry

[Chris Henson]

Hmm. I'll wait to think about this more carefully until the last sorry are filled in.

[Sehun Kim]

If you still have a interest in the locally closed hypothesis, the following would be helpful.

In [A. Chargueraud, The Locally Nameless Representation

](https://chargueraud.org/research/2009/ln/main.pdf), which is the primary reference of implementation, several different definitions of “locally closed” are proposed. One of them defines lc_at as

def lc_at (k : ℕ) (M : Term Var):Prop :=

match M with

| Term.bvar i => i<k

| Term.fvar _ => True

| Term.app t₁ t₂ => lc_at k t₁ ∧ lc_at k t₂

| Term.abs t => lc_at (k+1) t

One can prove that lc_at 0 M if and only if M.LC is closed and the function lc\_at yields more useful theorems. Proving it is little tricky, the induction on the number of lambdas in $M$ or “depth” of $M$ defined by

def depth (M : Term Var) : ℕ :=

match M with

| Term.bvar _ => 0

| Term.fvar _ => 0

| Term.app t₁ t₂ => Nat.max (depth t₁) (depth t₂)

| Term.abs t => depth t +1

is the best approach I found.

Using lc_at, we can prove the theorems like

theorem lc_at_iff_lc_at_openRec_fvar (M : Term Var) (x: Var) :

∀ i:ℕ , lc_at (i+1) M ↔ lc_at i (@openRec Var i (fvar x) M)

This means that M ^ fvar x is locally closed if and only if lc_at 1 M.

I think the main and only case we need to consider is the case when N=fvar x, and in this case, abs M is locally closed since lc_at 1 M holds.

[Chris Henson]

If you think it would be useful elsewhere, I'd be happy to review a separate PR adding this definition. It is probably best if it includes a proof that at level zero this is equivalent to our existing LC definition.

[Sehun Kim]

Actually I already made a proof.

[David Wegmann]

Maybe my intuition is wrong, but what @Sehun Kim proposes is maybe necessary to fill in the last sorry in my proof.

[David Wegmann]

my intuition for this is the following: Consider the open operation. it is not enough to define if just for replacing the 0th debrujin index, because it is recursively defined through incrementing the index to be replaced whenever one walks by an abstraction. But then proofs about such operations also require an induction hypothesis that is relative. We need a way to express that a term is "locally closed upto the last n levels" otherwise we cannot state such general enough induction hypotheses. I have a feeling that something like this is necessary to resolve the sorry in my file.

[Chris Henson]

I think there are some ways you can get around this, but I'm fine with this approach. I'd just ask that you split off what you can into smaller PRs to start with. Especially lc_at seems easy to do this for. This also applies to some of the lemmas in your draft PR that aren't specific to normalization.

[David Wegmann]

Alright, I'll do that, but I think most of the "not specific" to stlc strong norm lemmas are still very specific to strong norm lemmas in general. I'll try to get everything to compile first, then I'll break it up into multiple pull requests.

[Chris Henson]

I have merged @Sehun Kim's cslib#336 adding this more general version of local closure, so feel free to use it as needed for normalization.

[David Wegmann]

I used it and it worked perfectly. The strong norm proof file is now sorry free: https://github.com/WegmannDavid/cslib/blob/main/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
I still have to solve some sorries in the other file, then I will break it up and implement the style guide.

[David Wegmann]

Having worked with debruijn indices in the past, the definition of LcAt from @Sehun Kim feels much more natural and general enough than the current LC definition. If I were asked to come up with a definition for locally closedness, In retrospect I think I would have come up with exactly the same definition as @Sehun Kim .

[David Wegmann]

Appart from my intuition, I have a specific issue with the current LC definition. It requires one to pick a set of variables that are excluded in the abs case. This set is not uniquely determined, which makes LC a structure instead of a property.

[David Wegmann]

If I had to make the decision, I would replace LC with LcAt in the entire development.

[Chris Henson]

As the original paper that @Sehun Kim linked above mentions, I think there are some nice things about the inductive LC definition such as the induction principle it uses and that it hides the depth level which is irrelevant for most proofs. Especially in light of the other cofinite constructors, I think it is also more consistent and this is the standard way to formalize locally nameless binding.

I'm not quite sure the distinction you are drawing between "structure" and "property", but it is well-understood that these sets of variables are not unique. In fact the free_union term elaborator that is used throughout specifically takes advantage of this fact to allow specifying free variables at a high level. While I think it is useful to also have LcAt, I don't think I would agree with replacing LC entirely as I think in practice this would come with more bookkeeping. If you are very sure to the contrary I encourage you to try it out and I would carefully consider a PR that fully ports not just simple terms but System F as well.

Please also note that we are planning to support well scoped de Bruijn indices in the future which will align much more closely with what you are used to. It is not at all my intent to force all the lambda calculi modules in CSLib to use this locally nameless binding, which I agree can be a bit unintuitive. It is on my personal TODO list to port this for STLC/System F so that people have a example of either style and are free to choose for further type systems.

[David Wegmann]

That sounds reasonable. I don't have a strong opinion on it as I only have the viewpoint of somebody trying to contribute a single proof. I just wanted to offer that opinion in case everybody else is indifferent about LC vs LcAt. If the specific LC definition makes multiple other things simpler and just makes the strong norm proof a bit more tedious than I suppose it is reasonable to keep it that way.

[David Wegmann]

About SystemF: I have done full church style debruijn SystemF with strong norm and confluence and everything. The issue that comes up without something like autosubst is that you get a horrible combinatoric explosion of lemmas that let you move substitutions/steps/liftings between different levels of terms

[David Wegmann]

My coq debrujin stlc development was like 500 lines at the end, including confluence and strong norm.

The System F development was like 1000 lines. System F omega was 3000 lines I think.

[David Wegmann]

essentially every time you add another level of terms with their own substituions, you have get a quadratic increase of all the bookkeeping lemmas.

If you guys really want something like that I could port it, but I am not sure how much value it would add to the library. It would just be big and complicated.

[Chris Henson]

Yes, I agree. This is why I am working on something analogous to Autosubst for CSLib, but this is going to take me some time.

[David Wegmann]

@Chris Henson I just finished the entire proof for strong normalization, there are no more sorries left.
You can take a look at it if you want to, but I plan on simplifying the proof code before submitting a proper pull requests
https://github.com/WegmannDavid/cslib/tree/main

I was thinking about splitting the entire thing into 4 pull requests:

1. Add some required lemmas into existing files like FullBeta.lean and Properties.lean (some of these reside in my StrongNorm.lean as of now)
2. Add multiApp.lean + lemmas, operation that applies a list of argument terms to a term and lots of lemmas
3. general Strong Norm lemmas
4. strong norm proof for stlc.

Sounds good?

[Chris Henson]

Exciting! Yes, splitting things up is always appreciated. The first two sound good, though maybe if 3+4 are not too long, it is easier to review them together?

[David Wegmann]

alright. I'll still take a few days to shorten the proofs, then I'll know how long these will get.

[Chris Henson]

Feel free to open the first of the PRs even with minimal shortening, because I'll also work on this while reviewing.

[David Wegmann]

At the moment I am trying to spread the whole thing over multiple files

But there is an issue. Somehow, if I put multiApp into a different file called multiApp.lean, like this:

module

public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta

public section

namespace Cslib

universe u

variable {Var : Type u} [DecidableEq Var] [HasFresh Var]

namespace LambdaCalculus.LocallyNameless.Untyped.Term

@[simp]
def multiApp (f : Term Var) (args : List (Term Var)) :=
  match args with
  | []      => f
  | a :: as => Term.app (multiApp f as) a

I cannot rw/simp/unfold/ it any more.

even explicitly writing unfold Untyped.Term.multiApp in another file doesn't work for some reason
the term also doesn't appear to be definitionally equal to the terms it unfolds to.

[Chris Henson]

It looks like you are missing @[expose] public section. This is a recent change with the module system.

[David Wegmann]

Thanks, that fixed it.

[David Wegmann]

Could you quickly glance over this? I split the whole thing into multiple files. It's not split into multiple pull requests yet. I just want to know if you are happy with the number/theme of the files.

https://github.com/WegmannDavid/cslib/tree/main/Cslib/Languages/LambdaCalculus/LocallyNameless

[Chris Henson]

Is that the commit you meant to share? It has an empty file for multiple substitution and the strong normalization files seem to still have several lemmas about reduction, LcAt, etc. that should be moved.

[David Wegmann]

https://github.com/WegmannDavid/cslib/tree/main/Cslib/Languages/LambdaCalculus/LocallyNameless

[David Wegmann]

try it now, I think I forgot to save the file in vscode

[Chris Henson]

That looks better! There are still a few lemmas in Untyped/StrongNorm (step_subst_cong2 , steps_subst_cong2 , steps_open_cong_abs , lcAt_openRec_lcAt , open_abs_lc) that seem like they don't belong there. Unless I'm missing something, those are just general properties or about reduction.