Skip to content

Latest commit

 

History

History
142 lines (120 loc) · 5.9 KB

HACKING.md

File metadata and controls

142 lines (120 loc) · 5.9 KB
Raw

Personoj developer guide

This files provides an overview of the repository and some technical details.

  1. Repository architecture
  2. Continuous integration
  3. Why is the output of Personoj checked with a fork of Lambdapi?
    1. Lambdapi can't apply coercions with implicit arguments
    2. Coercions may create unsafe symbols
    3. Lambdapi can't coerce functions by itself
  4. Automated proof translation procedure

Repository architecture

  • encoding: encoding of PVS in Lambdapi
  • encoding.dk: encoding of PVS in Dedukti
  • mk: recipes to be used by BSD Make
  • pvs_patches: source code of personoj
  • tests: unit tests and procedures to translate and type check the Prelude of PVS
  • tools: scripts for the continuous integration and other tools

Continuous integration

The continuous integration checks that the encodings in encoding/ are accepted by lambdapi. It also runs the tests in tests/.

Why is the output of Personoj checked with a fork of Lambdapi?

The output of Personoj can only be typechecked wih a fork of Lambdapi which solves three issues with the main version.

Lambdapi can't apply coercions with implicit arguments

The main version of Lambdapi often fails to apply coercions in presence of implicit arguments. Coercion rules must filter types to be applied. Therefore, if a type is an existential variable, it won't match any pattern. In Lambdapi, existential variables are unified after type checking is done, and thus after coercions are applied. In particular, implicit arguments won't be instantiated before applying coercions.

For instance, let's define the following theory

constant symbol Set: TYPE;
symbol El: Set → TYPE;
constant symbol inhabited: Set → Set;
constant symbol inhabitant [a: Set]: El a → El (inhabited a);

Then define two encoded types nat and int

constant symbol nat: Set;
constant symbol z: El nat;
constant symbol int: Set;
constant symbol posint: El nat → El int;
coerce_rule coerce (El nat) (El int) $x ↪ posint $x;
coerce_rule coerce (El (inhabited $X)) (El (inhabited $Y)) (inhabitant $e)
          ↪ inhabitant [$Y] (coerce (El $X) (El $Y) $e);

Declare a function

symbol inhabitedInt: El (inhabited int) → TYPE;

Then typechecking inhabitedInt (inhabitant z) yields the following calls, where => is type inference, <= is type checking, = denotes unification constraints and the implicit argument is shown as an existential variable ?0

inhabitedInt (inhabitant ?0 z) => ...
	inhabitant ?0 z => El (inhabited ?0)
		inhabitant => Π a: Set, El (inhabited a)
		?0 <= Set
		z <= El ?0
			z => El nat
			El nat == El ?0
	inhabitant ?0 z <= El (inhabited int)
		El (inhabited ?0) = El (inhabited int)

Type checking fails because we obtain the constraints ?0 = nat and ?0 = int.

The solution implemented in the fork is to call the unification algorithm as soon as possible during type checking, that is, here. Thus, in the 7th line, ?0 is immediately unified with nat, and the 9th line El (inhabited nat) = El (inhabited int) becomes an instance of one of the coercion rules defined above.

Coercions may create unsafe symbols

Lambdapi reduces terms of the form coerce A B t to eliminate coerce from terms, and replace the type checked term with the reduced term. These reductions may generate unsafe symbols such as pair'.

For instance, in the Lambdapi encoding of Personoj, there is a coercion rule of the form

coerce_rule coerce (El $a) (El (psub $a $p)) $x ↪ pair $a $p $x _

But there is also a reduction from pair a p e h to pair' a p e, so the reduction (with strategy weak head normal form) will reduce to pair' a p e.

The fork introduces an advanced notion of opacity (in this commit), the symbol pair is declared opaque and the reduction involved in coercions does not use rewrite rules of opaque symbols.

Lambdapi can't coerce functions by itself

If one declares a coercion rule

coerce_rule coerce A B e ↪ f e;

it's not clear whether λ (_:C)(y:A),y will be coerced to λ(_:C)(y:A),(f y) if C → A → B is expected instead of C → A → A. In the fork, that coercion will happen. In Lambdapi 2.4.1, the coercion won't happen. The coercion can be recovered by adding the following coercion rule

coerce_rule coerce (Π a: $A, $B.[a]) (Π a: $A, $C.[a]) (λ a:$A, $e.[a])
          ↪ λ a:$A, coerce $B.[a] $C.[a] $e.[a]

See [[1]] section 3.1.4 for more details.

Automated proof translation procedure

The commit tagged 20220205 contains a set of procedures designed to prove automatically the inference steps of proofs of PVS using the tactic why3 of Lambdapi. It works as follows. For any theory, the proveit program can leave traces (in particular inference steps) of the proofs in the JSON format. Assuming the specification of the theory has been translated, the pipeline made of all procedures can generate a Lambdapi file that calls the why3 tactic on each inference step.

This method is deprecated in favour of a translation inside PVS of the inference steps. The latter method has been started with the function pprint-proof in pp-lp.lisp, but is not yet complete. See the documentation of pprint-proof for more information.

[1]: Expressing predicate subtyping in computational logical frameworks https://theses.hal.science/tel-03855351