An encoding of Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti
This repository contains the Dedukti theory presented in [1] encoding the Calculus of Constructions with cumulativity and product covariance, along with some files allowing to reproduce the results reported in the article.
To be able to reproduce all of our results, you will need to use a special version of Lambdapi, which features improved export functions. To install it with opam, just run
opam pin https://github.com/thiagofelicissimo/lambdapi.git#c21abb4
If you just want to check that the theory is well typed and preserves typing, a standard version of Lambdapi will do.
The theory is given in the Lambdapi file cc.lp. To check that the theory is well typed, you can run lambdapi check --no-sr-check --no-warnings cc.lp. The flag --no-sr-check disables the subject reduction checker: as explained in the article, the theory does not satisfy it for all terms, so Lambdapi cannot prove it automatically (see the subsection "Preservation of Typing" of this README for more details). The flag --no-warnings disables some unimportant warnings about left-hand side metavariable names that can be replaced by _.
It should succeed by only showing:
Checking "path-to-this-directory/cc.lp" ...
The proof of confluence of the theory given in the article proceeds by splitting the rewrite system into two systems local-confluence/ and strong-normalization/ one can find proofs of these facts which were generated by confluence provers CSI^ho and SOL, and termination prover APRoVE. We also give detailed instructions on how to reproduce our results.
The proof of subject reduction given in the article uses Lambdapi to check automatically that most rules preserve typing unconditionally, and also to calculate the constraints over which the other rules preserve typing.
In order to verify the preservation of typing for the group of rules that satisfy it unconditionally, first comment out lines 82, 86, 87, 89 and 90 of cc.lp. Then it suffices to run lambdapi check --no-warnings cc.lp.
In order to calculate the constraints for the rules that only preserve typing conditionally, we uncomment each rule separately and run lambdapi check --no-warnings cc.lp. The constraints associated with the rule are then printed by Lambdapi, but unfortunately in the output each $M is replaced by $n for some natural number n. For instance, by running the previous command with lines 82, 86, 89 and 90 commented out (meaning calculating the constraints of the rule on line 87), we get the output
Cannot solve $1 + $3 ≡ ($1 + $3) ∨ $1
Cannot solve S ($1 + $3) ∨ $1 ≡ S ($1 + $3)
Unable to prove type preservation.
An issue in the Lambdapi repository has already been opened in order to correct this behavior, however for the time being we can use an alternative method to find the names each natural number correspond to. To do this, in the file cc.lp we add debug +s; just before the rewriting rule we are checking that preserves typing, and run lambdapi check --no-warnings cc.lp again. Doing this for the example above gives the output
debug +s
[subj] π (S $0) (S $1) 0 (↑ $2 ⋄ $3) $4 ↪ ↑ (S ($0 + $1)) ⋄ (π (S $0) $1 0 $3 $4)
[subj] replace pattern variables by metavariables:
π (S ?1) (S ?3) 0 (↑ ?5 ⋄ ?7) ?9 ↪ ↑ (S (?1 + ?3)) ⋄ (π (S ?1) ?3 0 ?7 ?9)
...
The rest of the output is omitted, the information we want is given right after the line replace pattern variables....
By comparing with the rule as defined in cc.lp
rule π (S $l₁) (S $l₂) 0 (↑ _ ⋄ $A) $B ↪ ↑ (S ($l₁ + $l₂)) ⋄ (π (S $l₁) $l₂ 0 $A $B);
we see that $1 corresponds to $l₁ and $3 corresponds to $l₂. Repeating this process for all the rules on lines 82, 86, 87, 89, 90 allows us to calculate the constraints given in the article.
[1] Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti, Draft