Is anyone aware of any literature about implementing type checking/inference algorithm for CoC (or variant) with untyped conversion and using fuel (for purposes of termination) ? I am mostly interested in the proofs of soundness and completeness, I have seen an implementation in MetaCoq, but it was not verified, and I think this is really the tricky part.
did you see https://github.com/coq-contribs/coq-in-coq and its accompanying paper?
wow, Lemma type_sn : forall e t T, typ e t T -> sn T.
I wonder how they did that!
I skimmed the manuscript quicktly, and I think their idea was to model coq in some form of sets and use that model to show it is normalizing and then use the normalization result to provide dependability, which doesn't sound like a nice idea at least for my case.
i just want to completely avoid dealing with that and just work with partial correctiness using fuels, but I couldn't find good layouts for the proofs.
I think you can adapt the general idea of MetaCoq to the fuel setting: in case you return "yes", you also return a derivation (that you should have build on the way), and in case you return "no", you should construct a proof that your term is not typable. The only difference is that now you have a third case, where you run out of fuel. This gives you soundness of both kinds of answers.
However, completeness is probably not provable if you do not prove normalization. For instance, if you phrase completeness as if , then there exists some such that given fuel my conversion test answers "yes", this implies normalization. Indeed, you can show that whenever is typable, but then completeness implies that the conversion algorithms (which normalizes the terms given as input) will terminate on in finite time, effectively showing that is normalizing.
I see, this is more tricky than I thought, I am now wondering if assuming normalization is the most sensible choice
why do you need completeness?
(IMHO?) incomplete typecheckers can be fine, unless they're too limited. A proof won't tell you that your typechecker works in say 99.999% of cases so it's good enough in practice.
For instance, if you misuse C++ templates or Coq typeclasses, it's easy to cause infinite loops which make things incomplete.
A C++ compiler typically has a fixed maximal fuel for templates (say, 100), then is stops.
Coq is more generous and keeps running, but at some point the user will press Ctrl-C and _then_ it stops :-).
And even for the core theory, conversion checking isn't polynomial, and this can be a problem in practice. Again, Ctrl-C helps.
In both cases, a "correct" program fails to typecheck, but even if it's "correct", you're still going to fix it — maybe after asking questions here to understand how that's possible. And this isn't something that completeness can avoid!
well I used to see things different, I thought that the whole point of having proof is to make sure that all grounds are covered, and at least when I started, soundness and completeness felts like the two most basic properties every system must have
but I now see and start to agree with your point
I should point out: I suspect the _consensus_ agrees with you, and the one above is a less standard position
but you're not proving normalization, so you're not doing the standard thing anyway :wink: .
I am slightly confused, I thought that formal implementations never proved normalization ? due to godel incompleteness, is that wrong ?
walker said:
I am slightly confused, I thought that formal implementations never proved normalization ? due to godel incompleteness, is that wrong ?
Formalizing normalization proofs, especially for dependently typed language, is still a daunting task, so there are not many examples of it. But as long as your meta-theory (the one of the proof assistant you use) is logically stronger than the target theory (the one whose normalization you are proving), you in principle can formalize a normalization proof. See for instance this formalization, where they use induction-recursion in the meta-theory to formalize normalization of a theory that does not have it (although, they do not implement a type-checker, only a conversion-checker), @Loïc P's refinement which uses a meta-theory with more universe levels than the target language, or Coq in Coq, which formalizes normalization for CoC in full-blown CIC (more universes, and inductive types).
Paolo Giarrusso said:
(IMHO?) incomplete typecheckers can be fine, unless they're too limited. A proof won't tell you that your typechecker works in say 99.999% of cases so it's good enough in practice.
I think a good middle ground, which is more refined than simply letting go of completeness is to show that normalization is the only issue preventing the system to be complete. I don't think this has been explored a lot, but for instance there is A Partial Type Checking Algorithm for Type : Type, which shows that the type-checking algorithm in complete in a coinductive sense, which more or less corresponds to this idea.
I am slightly even more confused here, I am not sure, how can reduction algorithm be complete with respect to small step reduction,
In single step reduction, we have the following:
Inductive Reduction: Term -> Term -> Prop :=
...
| Reduction_beta: forall A t n, (appl (lam A t) n) ⟶ t.[n/]
| Reduction_appll: forall m m' n, m ⟶ m' -> (appl m n) ⟶ (appl m' n)
| Reduction_applr: forall m n n', n ⟶ n' -> (appl m n) ⟶ (appl m n')
...
where "t1 '⟶' t2" := (Reduction t1 t2).
That mean I can construct an a term that is possible to be reduced on all three fronts, and the reduction predicate does not enforce one or the other, but the algorithm must do so, which means that the reduction algorithm for single step may be sound, but I cannot prove it is complete at all, because it must pick an order for all those three possible steps.
When I say sound and complete this is what I have in mind:
Lemma reduction_sound t1 t2: reduction t1 = Some t2 -> t1 ⟶ t2.
Admitted. (*proved outside*)
Lemma reduction_complete t1 t2: t1 ⟶ t2 -> reduction t1 = Some t2.
Admitted. (*apparently does not hold because the reduction must pick an order *)
I thought that that means for multi step reduction it will get better, but it does not because Multistep reduction relation does not require progress to be made at all:
Inductive Multi (R: Term -> Term -> Prop): Term -> Term -> Prop :=
| Multi_refl: forall t, Multi R t t
| Multi_single: forall t1 t2 t3,
R t1 t2 ->
Multi R t2 t3 ->
Multi R t1 t3.
On the other hand, the algorithm equivalent will try to get the best possible reduct, I am worried that those problems will keep propagating, and realize very late that I cannot prove completeness (or partial completeness) because I missed something important
So how can completeness lemmas be formalized for those two cases?
It depends on what exactly your reduction algorithm implements, but the simplest form of completeness is something like
Lemma reduction_complete t1 t2 : Multi Reduction t1 t2 -> normal_form t2 -> reduction t1 = t2
ie whenever t
reduces to a normal form, the reduction algorithm finds that normal form.
right!, it makes sense, I think this is provable (taking into account dealing with fuel and having partial results ..etc)
but my multi_reduce function is very simple:
Equations multi_reduce (fuel: nat) (t: Term) : Result Term :=
multi_reduce 0 _ := Err OutOfFuel;
multi_reduce (S fuel) t := match reduction t with
| None => Ok t
| Some t' => multi_reduce fuel t'
end.
it should just go to normal form, the reduction
function is like the default reduction inductive type but with just setting some arbitrary order.
I think for my case, the lemma would be something like:
Lemma reduction_complete fuel t1 t2 : Multi Reduction t1 t2 -> normal_form t2 -> multi_reduction t1 =Some t2 \/ multi_reduction t1 = Err OutOfFuel.
If there is something I should also take into account feel free to let me know!
This looks good to me :)
I don't think this is an interesting result, because the function that always returns OutOfFuel
satisfies it. You should instead prove that there exists enough fuel to actually end up with t2
.
(Possibly, you might need the excluded middle, or prove the converse.)
mmm, I see your point, but that is strong normalization, which I wanted to avoid proving ?
I am intending to add features to my experimental toy language that might be stronger than what coq can offer (HITs) so I want to avoid worrying about normalization
No, you are supposing normal_form t2
, so this is much weaker than strong normalization. It is just plain confluence toward the normal form.
isn't strong normalization saying (at least informally) that every well typed expression will eventually be reduced to normal form ?
Yes.
isn't that the same as saying that there exists enough fuel to get there ? (which you just described)
No, what I am describing is that, if a term can be reduced to a normal form, your algorithm will eventually also reach that normal formal. And this is just a corollary (by definition of a normal norm) of the fact that, if a term can be reduced to a normal form, your algorithm cannot exhibit an infinite sequence of reductions.
I see, I wonder how hard will it be to prove that, I will actually try it and see where I get stuck!
thanks a lot for the idea!
Ah, indeed, you're right, thanks for the catch!
If reduction were deterministic, the needed fuel would just be the length of the multi reduction sequence. OTOH, with non-determinism and a system that is WN but not SN (say, naive explicit substitutions + beta) I'm not sure how Guillaume's proof works because you can exhibit an infinite reduction sequence?
You need instead to prove that your algorithm avoids that infinite sequence.
I'm not sure you can, and I don't know myself for explicit substitutions + beta (not an expert). OTOH, untyped lambda calculus doesn't have normalization, but this theorem is false for call-by-value evaluation and true for lazy evaluation (when not reducing under lambdas)
and when reducing under lambdas, IIRC/IIUC the result can be proven via the standardization theorem for reduction in normal order
Paolo Giarrusso said:
You need instead to prove that your algorithm avoids that infinite sequence.
Note that is exactly what I said: "this is just a corollary [...] of the fact that [...] your algorithm cannot exhibit an infinite sequence of reductions."
I'm not sure I follow because in these cases the infinite sequence exists:
you can have t1 ->* t2
, t2 normal
, yet there exists an infinite reduction sequence starting from t1
Sure, but can the algorithm follow it? You have to prove that it cannot. That is my point.
okay, we're in agreement
I was thrown off by "confluence toward the normal form"
What I mean by that is that you have to prove that, if two sequences of reduction lead to irreducible terms, then these terms are actually equal. (In other words, this is the existence of a normal form.) For example, in an untyped lambda-calculus with explicit substitutions, this is not always true. You can only prove that the two irreducible terms are equivalent modulo erasure of the explicit substitutions (or you need to add some extra reduction rules to your calculus).
okay, that sounds like confluence. I thought "normal" and "irreducible" coincided...
it all checks out
So here is my progress regarding proving
Lemma multi_reduce_complete t1 t2: t1 ⟶* t2 -> NormalForm t2 -> exists fuel, multi_reduce fuel t1 = Ok t2.
This property was a direct consequence of another lemma:
Lemma multi_reduce_preservation fuel t1 t2 t3:
multi_reduce fuel t2 = Ok t3 -> t1 ⟶ t2 -> exists fuel', multi_reduce fuel' t1 = Ok t3.
Here I processed by induction over the stucture the single stepping judgement, and I was stuck at one case regarding the beta reduction:
In the judgement, the beta reducttion rule is given as follows:
Inductive Reduction: Term -> Term -> Prop :=
...
| Reduction_beta: forall A t n, (appl (lam A t) n) ⟶ t.[n/]
...
The problem is that the induction hypthesis is not strong enough and during in multi_reduce_preservation
I get a case that i:
t1, t2, n, t3: Term
fuel: nat
Hmred: multi_reduce fuel t2.[n/] = Ok t3
====================================== Goal
exists fuel' : nat, multi_reduce fuel' (appl (lam t1 t2) n) = Ok t3
The problem here is that unlike the induction principle for pi
, lam
and other constructs, we canoot establish any fact about t1, t2 or t3 on it own, and the substitution presented by t2.[n/]
is not a primative construct but an operation
The closest thing I was able to do is prove that :
Lemma multi_reduce_trans_appl_beta A f m n n' t fuelm fueln fuelapp:
multi_reduce fuelm m = Ok (lam A f) ->
multi_reduce fueln n = Ok n' ->
multi_reduce fuelapp (f.[n'/]) = Ok t ->
exists fuel, multi_reduce fuel (appl m n) = Ok t.
But to use that, I need to know if what each Term reduces to on its own and that was not available in case of beta reduction. It will cool if anyone has idea possible paths on how to proceed.
this depends on the definition of multi_reduce
we canoot establish any fact about t1, t2 or t3 on it own
but is it necessary to have such facts?
Yeah I tried proving them from multi_reduce fuelapp (f.[n'/]) = Ok t
By induction over fuel, but it never worked.
let me retry quickly and get the problem.
yup, here we go, I will have to also share how multi_reduce work:
Equations multi_reduce (fuel: nat) (t: Term) : Result Term :=
multi_reduce 0 _ := Err OutOfFuel;
multi_reduce (S fuel) t := match reduce t with
| None => Ok t
| Some t' => multi_reduce fuel t'
end.
So if I try deduce one of the two facts from the substution:
forall f n t fuel,
multi_reduce fuel (f.[n/]) = Ok t ->
exists fueln n', multi_reduce fueln n = Ok (n').
I proceeded by induction over fuel (nat), the first case istrivial because the assumption becomes: Err OutOfFuel = Ok t
The second case is:
multi_reduce fuel.+1 f.[n/] = Ok t ->
exists (fueln : nat) (n' : Term), multi_reduce fueln n = Ok n'
While the induction hypothesis is:
IHfuel: forall f n t : Term, multi_reduce fuel f.[n/] = Ok t -> exists (fueln : nat) (n' : Term), multi_reduce fueln n = Ok n'
Which is bad sign, becaue the second argument for multi_reduce
must always be f.[n/]
But I proceed anyways by simplification and I get:
match reduce f.[n/] with
| Some t' => multi_reduce fuel t'
| None => Ok f.[n/]
end = Ok t ->
exists (fueln : nat) (n' : Term), multi_reduce fueln n = Ok n'
I case analyse reduce f.[n/]
and one of the cases looks like ( I didn't bother checking the other case):
multi_reduce fuel red' = Ok t ->
exists (fueln : nat) (n' : Term), multi_reduce fueln n = Ok n'
This does not match the induction hypothesis, and no way to make look like the x.[y\]
pattern.
ofcourse the obvious solution would have the lemma with 1 layer of indirection:
forall f n t fuel X,
multi_reduce fuel = Ok t ->
X = (f.[n/]) ->
exists fueln n', multi_reduce fueln n = Ok (n').
but you get the same problem but in a slightly different form.
this unfortunately one of the cases, where I just run out of ideas to try and wonder if there is a new tricks I can add to my toolbox for this particular case.
I can share the whole code for anyone who would be interested.
but in the original goal
t1, t2, n, t3: Term
fuel: nat
Hmred: multi_reduce fuel t2.[n/] = Ok t3
====================================== Goal
exists fuel' : nat, multi_reduce fuel' (appl (lam t1 t2) n) = Ok t3
shouldn't reduce (appl (lam t1 t2) n) = Some t2.[n/]
? so you can just do exists (S fuel); exact Hmred
Not really, Let me show you the definition of reduce:
and you never care about multi_reduce _ n
| appl m n => match reduce m with
| Some m' => Some (appl m' n)
| None => match reduce n with
| Some n' => Some (appl m n')
| None => match m with
| lam A e => Some (e.[n/])
| _ => None
end
end
end
change it to do the match m
first, problem solved?
I first reduce m
thenreduce n
then perform the subsitution if reduction of m was lam _ _
I thought about that, but my intution tell me that this problem will appear again when I need to do some operations on m
and n
because now i will have to get through the reduction first.
Isn't the point of multi_reduce is that reduce does a single step?
yes it does ?
does it not ?
I mean, reduce shouldn't be recursive, it should do a single small step
Not saying you won't get other questions, but if the new setup makes more sense they'll be better questions
I say if because it's up to you to choose the general setup
I am not sure how it will not be recursive.
let me show you the judgement part and the algrorithm
Reserved Notation "x '⟶' y" (at level 20, y at next level).
Inductive Reduction: Term -> Term -> Prop :=
| Reduction_beta: forall A t n, (appl (lam A t) n) ⟶ t.[n/]
| Reduction_pil: forall A A' B, A ⟶ A' -> (pi A B) ⟶ (pi A' B)
| Reduction_pir: forall A B B', B ⟶ B' -> (pi A B) ⟶ (pi A B')
| Reduction_laml: forall A A' t, A ⟶ A' -> (lam A t) ⟶ (lam A' t)
| Reduction_lamr: forall A t t', t ⟶ t' -> (lam A t) ⟶ (lam A t')
| Reduction_appll: forall m m' n, m ⟶ m' -> (appl m n) ⟶ (appl m' n)
| Reduction_applr: forall m n n', n ⟶ n' -> (appl m n) ⟶ (appl m n')
where "t1 '⟶' t2" := (Reduction t1 t2).
Notation "x '⟶*' y" :=
(Multi Reduction x y) (at level 20, y at next level).
Fixpoint reduce (t: Term) : option Term :=
match t with
| var idx => None
| univ l => None
| pi A B => match reduce A with
| Some A' => Some (pi A' B)
| None => match reduce B with
| Some B' => Some (pi A B')
| None => None
end
end
| lam A t => match reduce A with
| Some A' => Some (lam A' t)
| None => match reduce t with
| Some t' => Some (lam A t')
| None => None
end
end
| appl m n => match reduce m with
| Some m' => Some (appl m' n)
| None => match reduce n with
| Some n' => Some (appl m n')
| None => match m with
| lam A e => Some (e.[n/])
| _ => None
end
end
end
end.
IIRC you're in a possibly non terminating system
I think that means you have to do the match m
first
consider loop
a term with no normal form and n
some closed normal form
by beta appl (lam n n) loop
reduces to n
which is normal
but by your algorithm multi_reduce
will keep working on loop
and never finish
Paolo Giarrusso said:
I mean, reduce shouldn't be recursive, it should do a single small step
it's recursive because it does subterms
okay, I agree with Gaëtan
basically you implemented some kind of "call by value with eager reduction under binders" but you need call by name
Gaëtan Gilbert said:
I think that means you have to do the
match m
first
considerloop
a term with no normal form andn
some closed normal form
by betaappl (lam n n) loop
reduces ton
which is normal
but by your algorithmmulti_reduce
will keep working onloop
and never finish
I will try since this is the onyl option left, but I feel it will not work when doing the general case of appl m n
. my intution is based on the fact that this reduction system is confluent so order of operations should not matter.
no, confluence doesn't help here
Gaëtan Gilbert said:
basically you implemented some kind of "call by value with eager reduction under binders" but you need call by name
This is one the things I never understood, It is on my to-learn-about list, if there is an good survery that the goto I will be happy if you let me know about it.
untyped lambda calculus is confluent, yet we know call-by-name finds strictly more normal forms
as for the order of operations I will be super happy to learn that my intution was wrong, I will try it and let you know the end result.
you should work through Gaëtan's example before doing that
the proof might still run into technical challenges, but I think he simply gave a counterexample
you can also tell from the statement of confluence: it doesn't guarantee that every order will find the normal form, only that whatever sequences of steps you take, there exists another sequence that will get to a common reduct
and that's why strong normalization and weak normalization are different properties, and WN does not imply SN
I have 1 last question, what if what i want is call by value ?
then it's false that your algorithm will always find a normal form that exists
you could make that true by weakening the overall reduction, but it'd be very strange in a dependently-typed language?
I am worried that call by name might not be what I really want, because my goal was at somepoint was to add some sort of side effects & be able to generate assembly instructions, and what worries me is that every language that have the same goal (but not necessarily dependent types) are call by value.
anyways, I will try to get it to work in call by name dealing side effect/assembly will be problems for future me.
as a side note — this helper lemma might have a common problem that you might want to learn about:
forall f n t fuel,
multi_reduce fuel (f.[n/]) = Ok t ->
exists fueln n', multi_reduce fueln n = Ok (n').
if f
does not mention var 0
, then f.[n/]
does not contain n
, so you can't deduce much about n
?
more generally, there exists research on dependent types + effects that you might need to look into
I've found https://ieeexplore.ieee.org/abstract/document/8005113 https://dl.acm.org/doi/abs/10.1145/3341712 https://arxiv.org/abs/1512.08009, but I'm not a specialist so I'm not sure what's the best reference.
But one point I can recognize: two of those papers mention call-by-push-value, which is a technique to get _both_ full reduction, while sequencing effects like in call-by-value
ah, https://www.reddit.com/r/dependent_types/comments/dq1zlt/side_effects_and_dependent_types/ recommends instead https://www.xn--pdrot-bsa.fr/articles/dcbpv.pdf — I can't find later papers by @Pierre-Marie Pédrot that seem relevant
thanks! I will read through them
to the best of my knowledge, the approach for algebraic side effects is not the best when it comes to proving stuff about them (which is I think the whole point of dependent types) so when I was saying side effects, I had monads in mind, but I will still read the papers, it is good idea to to familiarize myself with call-by-push-value.
I think CBPV predates algebraic effects, but even monads are fine with call-by-name
(but I'm not implying monad would mix well with dependent types, so it still seems good reading)
I am reading and I see a "stack", by any chance, is that the stack used in metacoq's type checker ?
I know that metacoq's typechecker uses a stack for something but never knew why!
FWIW, dependent types are heavily biased towards call-by-name.
If you go through the cbv-into-cpbv encoding with dependent cbpv you'll get a weird stuff probably nobody wants to consider.
If your plan is to get a programming language you'd probably better follow the PML path.
I literally read the first line and it says, The language is Curry-style and call-by-value. now I am confused as to which one is the go-to for dependent types ?
it's technically not based on dependent types, although the surface language looks a lot like it
it's closer to systems from the PRL family
(you can argue that PRL is a model of dependent types, but there not strictly speaking your off-the-shelf implementation of MLTT)
Last updated: Dec 01 2023 at 06:01 UTC