Are you familiar with CwFs?

The implementation is not simple to understand because we want algorithmic efficiency, but basically a substitution is just a list of terms

CwFs -> calculus with explicit substitutions, or are you talking about something else?

Yes I understand substitutions on paper but I struggle a bit with the de Bruijn manipulations involved

CwF are categories with families indeed

what part are you struggling with exactly? if you just assume they're lists of terms, then they have the expected typing rules of substitutions from CwFs

Pierre-Marie Pédrot said:

CwF are categories with families indeed

Oh in this case no I am not familiar with these. Do you have a good introductory resource (paper / course notes) on CwFs ?

I guess that depends on your background, it's often presented in contrived categorical ways

My categorical background is relatively weak I would say...

okay, so maybe it's not so worthwhile

Probably not indeed. I'll have to go back to the drawing board I guess

maybe we can try to do this interactively, it's a rather simple concept

if you have a term Γ ⊢ t : A, you can plug terms in the variables

substitutions are just a list of terms you can plug

in the variables of gamma right ?

a substitution Γ ⊢ σ : Δ is a list of terms that live in context Γ

yes

if you ignore dependency for a second, in the rule above Δ is just a list of types

ok

the base operation is that, given Δ ⊢ t : A and Γ ⊢ σ : Δ, you can plug into the variables of t the elements of σ and get Γ ⊢ t{σ} : A{σ}

ok

a trivial case is the one-element substitution Γ ⊢ [u] : B which is formed of Γ ⊢ u : B

Ah I see so it's the usual substitution lemma

indeed

in Γ ⊢ σ : Δ, the typing invariants guarantees that the length of σ and Δ are the same

yes

that's about it actually

we have one more trick in the Coq implementation, which is that we represent variables freely

so that the type of substitutions is polymorphic in its elements

that is, normally you have only two basic ways to build a substitution

which two ways ?

the empty substitution Γ ⊢ [] : ε

and cons, i.e. if Γ ⊢ σ : Δ and Γ ⊢ u : A{σ} then Γ ⊢ σ ++ [u] : Δ, A

(I hope I got it right and that it's well-typed, let's check)

looks good to me

but then what about `subs_lift: 'a subs -> 'a subs`

?

assuming Δ ⊢ A : Type we have Γ ⊢ A{σ} : Type, so this is fine

so this one is the "free" variable

what do you mean the free variable ?

i.e. if Γ ⊢ σ : Δ, then Γ, x : A ⊢ σ ++ [x] : Δ, x : A

(this is ill-typed so I'm missing a substitution somewhere)

but basically that means that you have one more variable in the context and you just use that one

it's the primitive you should use when you cross a binder in a term

oh so x is mapped to x

ah because we don't want to substitute bound variables

typically, (λx.t){σ} ≡ λx.t{lift(σ)}

yes makes sense

(you can infer the correct typing rule with that)

probably Γ, x : A{σ} ⊢ σ ++ [x] : Δ, x : A

yes we need to apply σ in A

in theory you could derive lift from other basic primitives on terms, but for efficiency and generality it's a primitive

the other similar primitive is shifting, which is just weakening of the context

so `subst_id`

is the empty substitution

yes

`subst_cons`

is adding an element to the substitution

yes

`subst_lift`

is the same but the variable is mapped to itself

yes

but what about `subst_shft`

?

that one is the one I mentioned above, it's weakening of the source context

weakening of Γ ?

in general if you have a term Γ ⊢ t : A you can build Γ, x : X ⊢ t{↑} : A{↑}

shift is the application of this weakening primitive to the whole substitution

so if Γ ⊢ σ : Δ then Γ, x : X ⊢ shift(σ) : Δ{↑}

where Δ{↑} is defined pointwise

(if you use bound variables rather than the de Bruijn indices this is just the identity)

basically you add an unused variable in the source context

oh this makes sense ! Something that was confusing me was that I hadn't realized that there were actually two forms of lifting that made sense for substitution : shifting and lifting, and I was kind of mixing both in my head

lifting is natural when going under contexts, while shifting is natural when substituting

(i.e. expressing the composition of substitution needs shifting)

yes I see (although I'll have to go through some examples myself)

as for the implementation itself, it is a bit subtle, I should have written a paper about it some time ago already

instead of lists it uses a variant of Okazaki's skewed-binary random access lists

so you get O(1) cons / shift / lift and O(log n) access in the substitution

yes I saw this indeed

but anyways I'm just looking to implement a naive version of substitutions, I don't need to get fancy with skewed lists

this is so far my one and only contribution to the inscrutable field of algorithmics, as this precise algorithm is AFAICT new

out of curiosity why do you want to reimplement this?

haha and now it's burried deep in Coq

so I'm working (as part of an M2 internship) on a prototype of a graphical interface for Coq with Benjamin Werner, and to my despair it's turning into a mini-theorem prover as I have to re-implement (simplified versions) many classical algorithms (on CC right now, but eventually probably something like CIC)

ah, the standard trick to lure in people with GUIs into type theory...

well personally I think GUIs have some potential for easing proof development as a supplement to traditional proof scripting, e.g. I've seen cool stuff being done in Lean

but alas not many people seem interested at the moment

well anyways thanks a lot for your explanations, that was very kind of you

Mathis Bouverot-Dupuis has marked this topic as resolved.

Do you have a good introductory resource (paper / course notes) on CwFs ?

Pierre-Marie Pédrot: I guess that depends on your background, it's often presented in contrived categorical ways

Papers relying on a type-theoretical approach that I found interesting are:

- Fridlender and Pagano, "Pure type systems with explicit substitutions", which basically is presenting CwF as a type system. This is in the "extrinsic style", i.e. with explicit proof terms and a conversion rule, while the initial structure of official CwFs is in the "intrinsic style", i.e. with only derivations and an equality on the derivations. (The paper does not have the η-rules of CwF either if I'm correct.)
- The literature from Kaposi and co-authors, e.g. Definition 2 in Kaposi, Kovács and Lafont, "For Finitary Induction-Induction, Induction Is Enough", which also presents CwF as a signature of types, constructors and equalities, which, if you put the keyword "Inductive" in front of the signature, you get the definition of a type system, and if you put instead the keyword "Record" in front of it, you get the official definition of CwF.

I myself once wrote a variant of CwF as a type theory where n-ary substitution is replaced by unary substitution in these notes. There is an open question: can we orient the equations as a normalizing rewriting system? It seems yes if we have only the bare structure (just axioms and substitutions) but probably no if we add Π and ∑ (the objective was to connect the works from the 90s on the n-ary - i.e. `esubst.ml`

-like - and unary - i.e.`Vars.liftn`

-like - schools on explicit substitution to the dependent type case). (I failed to answer positively to the question but maybe it is just that I missed something.) In the notes, I also explore to which extent proof-terms could be rethought as just "light" notations for derivations where some arguments are left implicit. (And I also explore how heterogeneous equality can be used to give a nicer presentation of the dependent typing system for explicit substitutions when the typing of the reduction of terms depends on the ability to reduce in types.)

Something that was confusing me was that I hadn't realized that there were actually two forms of lifting that made sense for substitution : shifting and lifting, and I was kind of mixing both in my head

Coq's implementation actually introduced some confusion. For some reasons (unknown to me), Coq swapped the shift/lift terminology compared to the ordinary literature (i.e. the usual literature call weakening "shift").

(And writing a paper about the algorithm would be good!)

Hugo Herbelin said:

Coq's implementation actually introduced some confusion. For some reasons (unknown to me), Coq swapped the shift/lift terminology compared to the ordinary literature (i.e. the usual literature call weakening "shift").

we can also see that lift_constr uses subs_shft

Last updated: Oct 13 2024 at 01:02 UTC