Need help with Dedukti?

Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

146 Stars 16 Forks Other 2.1K Commits 34 Opened issues

Implementation of the λΠ-calculus modulo rewriting

Readme

Note that a new interactive version of Dedukti is under development on https://github.com/Deducteam/lambdapi.

For interoperability developement, the current version of Dedukti is still used.

To compile (and optionally install)

Deduktiyou will need: -

OCaml >= 4.06, -

Menhir, -

dune, -

cmdliner, -

z3(universo only), -

odoc(doc only).

opam install dedukti

The current version on

opamis too old and we recommand to install Dedukti by cloning this repository.

git clone https://github.com/Deducteam/Dedukti.git cd Dedukti make make install

The command

bash dkcheck examples/append.dkshould output the following.

SUCCESS File 'examples/append.dk' was successfully checked.

See the

editorsdirectory. Only the emacs mode is maitained currently.

The installation provides the following commands: -

dkcheckis the type-checker for

Dedukti, -

dktopis an interactive wrapper around the type-checker, -

dkdepis a dependency generator for

Deduktifiles, -

dkpruneis a program to re-print only the strictly required subset of

Deduktifiles, -

dkprettyis a source code beautifier for

Dedukti, -

dkmetais a tool which uses

Deduktirewrite rules to rewrite a

Deduktifile, -

universois a tool which allows to work with universes using the encoding of

The Calculus of Inductive Constructionsin

Dedukti.

dkcheckprovides the following options: -

-eGenerates an object file

.dko; -

-I DIRAdds the directory

DIRto the load path; -

-d FLAGSenables debugging for all given flags: *

q(

n(

o(m

#REQUIRE), *

c(

-ccused), *

u(r

t(

r(

m(

-vVerbose mode (equivalent to

-d montru; -

-qQuiet mode (equivalent to

-d q; -

--no-colorDisables colors in the output; -

--stdin MODParses standard input using module name

MOD; -

--coc[Experimental] Allows to declare a symbol whose type contains

Typein the left-hand side of a product (useful for the Calculus of Construction); -

--type-lhsForbids rules with untypable left-hand side; -

--snfNormalizes the types in error messages; -

--confluence CMDSets the external confluence checker command to

CMD; -

--beautifyPretty printer. Prints on the standard output; -

--versionPrints the version number; -

--helpPrints the list of available options.

Then we can declare constants, giving their name and their type.

Deduktidistinguishes two kinds of declarations:

- declaration of a
*static*symbolf

of typeA

is writtenf : A

, - declaration of a
*definable*symbolf

of typeA

is writtendef f : A

.

Definable symbols can be defined using rewrite rules, static symbols can not be defined.

Nat: Type. zero: Nat. succ: Nat -> Nat. def plus: Nat -> Nat -> Nat.

Let's add rewrite rules to compute additions.

[ n ] plus zero n --> n [ n ] plus n zero --> n [ n, m ] plus (succ n) m --> succ (plus n m) [ n, m ] plus n (succ m) --> succ (plus n m).

When adding rewrite rules,

Deduktichecks that they preserve typing. For this, it checks that the left-hand and right-hand sides of the rules have the same type in some context giving types to the free variables (in fact, the criterion used is more general, see below), that the free variables occurring in the right-hand side also occur in the left-hand side and that the left-hand side is a

**Remark:** there is no constraint on the number of rewrite rules associated with a definable symbol.
However it is necessary that the rewrite system generated by the rewrite rules together with beta-reduction
be confluent and terminating on well-typed terms. Confluence can be checked using the option

-cc(see below), termination is not checked (yet?).

**Remark:** Because static symbols cannot appear at head of rewrite rules, they are injective with respect to conversion and this information can be exploited by

Deduktifor type-checking rewrite rules (see below).

A development in

Deduktiis usually composed of several files corresponding to different modules. Using

dkcheckwith the option

-ewill produce a file

my_module.dkothat exports the constants and rewrite rules declared in the module

my_module. Then you can use these symbols in other files/modules using the prefix notation

my_module.identifier.

In

Dedukticomments are delimited by

(;and

;).

(; This is a comment ;)

Supported commands are:

#EVAL t. (; evaluate t to its strong normal form and display it. ;) #EVAL[N]. (; same as above, but evaluate in at most N steps. ;) #EVAL[STRAT]. (; evaluate t with the strategy STRAT. :) #EVAL[N,STRAT]. (; same as above, but evaluate in at most N steps. :) #CHECK t1 == t2. (; display "YES" if t1 and t2 are convertible, "NO" otherwise. ;) #CHECK t1 : t2. (; display "YES" if t1 has type t2, "NO" otherwise. ;) #CHECKNOT t1 == t2. (; display "YES" if t1 and t2 are not convertible, "NO" otherwise. ;) #CHECKNOT t1 : t2. (; display "YES" if t1 does not have type t2, "NO" otherwise. ;) #ASSERT t1 : t2. (; fail if t1 does not have type t2. ;) #ASSERT t1 == t2. (; fail if t1 is not convertible with t2. ;) #ASSERTNOT t1 : t2. (; fail if t1 does have type t2. ;) #ASSERTNOT t1 == t2. (; fail if t1 is convertible with t2. ;) #INFER t1. (; infer the type of t1 and display it. ;) #PRINT s. (; print the string s. ;)

The supported evaluation strategies are: -

SNF(strong normal form: a term

tis in

SNFif no reduction can occur in

t), -

WHNF(weak head normal form: a term

tis said in

WHNFif there is a finite sequence

t=t0,

t2, ...,

tnsuch that

tnis in normal form and for all

i,

tireduces to

t(i+1)and this reduction does not occur at the head).

Note that the

#INFERcommand accepts the same form of configuration as the

#EVALcommand. When given, it is used to evaluate the obtained type.

Deduktisupports definitions:

def three : Nat := succ ( succ ( succ ( zero ) ) ).

or, omitting the type,

def three := succ ( succ ( succ ( zero ) ) ).

A definition is syntactic sugar for a declaration followed by a rewrite rule. The definition above is equivalent to:

def three : Nat. [ ] three --> succ ( succ ( succ ( zero ) ) ).

Using the keyword

thminstead of

defmakes a definition

thm three := succ ( succ ( succ ( zero ) ) ).

This can be useful when the body of a definition does not matter (only its existence matters), to avoid adding a useless rewrite rule.

When a variable is not used on the right-hand side of a rewrite rule, it can be replaced by an underscore on the left-hand side. In the following definition:

def mult : Nat -> Nat -> Nat. [ n ] mult zero n --> zero [ n, m ] mult (succ n) m --> plus m (mult n m).

the first rule can also be written:

[ ] mult zero _ --> zero.

Similarly underscores can replace unused abstracted variables in lambdas:

x => y => z => zerocan be written

_ => _ => _ => zero. Be mindful that, in a pattern, the expression

_ => _means

x => Ywhere both

xand

Yare fresh variables occuring nowhere else.

A typical example of the use of dependent types is the type of Vector defined as lists parametrized by their size:

Elt: Type. Vector: Nat -> Type. nil: Vector zero. cons: n:Nat -> Elt -> Vector n -> Vector (succ n).

and a typical operation on vectors is concatenation:

def append: n:Nat -> Vector n -> m:Nat -> Vector m -> Vector (plus n m). [ n, v ] append zero nil n v --> v [ n, v1, m, e, v2 ] append (succ n) (cons n e v1) m v2 --> cons (plus n m) e (append n v1 m v2).

These rules verify the typing constraint given above: both left-hand and right-hand sides have the same type.

Also, the second rule is non-left-linear; this is usually an issue because in an untyped setting, non-left-linear rewrite rules usually generate a non-confluent rewrite system when combined with beta-reduction.

However, because we only intend to rewrite *well-typed* terms, the rule above is computationally equivalent to the following left-linear rule:

[ n, v1, m, e, v2, x ] append x (cons n e v1) m v2 --> cons (plus n m) e (append n v1 m v2).

Deduktiwill also accept this rule, even if the left-hand side is not well-typed, because it is able to detect that, because of typing constraints,

xcan only be instantiated by a term of the form

succ n(this comes from the fact that

Vectoris a static symbol and is hence injective with respect to conversion: from the type-checking constraint

Vector x = Vector (succ n),

Deduktideduces

x = succ n).

For the same reason, it is not necessary to check that the first argument of

appendis

zerofor the first rule:

[ n, v, x ] append x nil n v --> v.

Using underscores, we can write:

[ v ] append _ nil _ v --> v [ n, v1, m, e, v2 ] append _ (cons n e v1) m v2 --> cons (plus n m) e (append n v1 m v2).

Declaring a symbol as

injectivemay help the type checker. Hence, it is possible to declare a symbol injective. However, no injectivity check is performed by the typechecker but the injectivity will be assumed and used when typechecking rules defined later on.

inj double : Nat -> Nat. [ ] double zero --> zero. [ n ] double (succ n) --> succ (succ (double n)).

Declaring a non-injective symbol as injective may break the injectivity of product, and therefore may break subjection reduction.

Variables in the context of a rule may be annotated with their expected type. It is checked that the inferred type for annotated rule variables are convertible with the provided annotation.

[ n : Nat , v1 : Vector n , m : Nat , e : Elt , v2 : Vector m ] append _ (cons n e v1) m v2 --> cons (plus n m) e (append n v1 m v2).

By default,

Deduktiaccepts non-left-linear rewrite rules even though they usually generated non confluent rewrite systems when combined with beta-reduction.

eq: Nat -> Nat -> Bool. [ n ] eq n n --> true.

This behaviour can be changed by invoking

dkcheckwith the option

--ll(left-linear) to guarantee that non-left-linear rewrite rules are never added to the system.

In the previous examples, left-hand sides of rewrite rules were first-order terms. In fact,

Deduktisupports a larger class of left-hand sides:

A *higher-order pattern* is a beta-normal term whose free variables are applied to (possibly empty) vectors of distinct bound variables.

A classical example of the use of higher-order rules is the encoding the simply types lambda-calculus with beta-reduction:

type: Type. arrow: type -> type -> type.term: type -> Type.

def app: a:type -> b:type -> term (arrow a b) -> term a -> term b. lambda: a:type -> b:type -> (term a -> term b) -> term (arrow a b).

[ f, arg ] app _ _ (lambda _ _ (x => f x)) arg --> f arg.

**Remark:** type annotations on abstraction *must* be omitted.

**Remark:** free variables must be applied to the same number of arguments on the left-hand side and on the right-hand side
of the rule.

**Remark:** with such rewrite rules, matching is done modulo beta in order to preserve confluence.
This means that, in the context

(o: type)(c:term o), the term

App o o (Lam o o (x => x)) creduces to

c.

A different solution to the same problem is to mark with brackets the parts of the left-hand side of the rewrite rules that are constrained by typing.

[ n, v1, m, e, v2 ] append (succ n) (cons {n} e v1) m v2 --> cons (plus n m) e (append n v1 m v2).

The information between brackets will be used when typing the rule but they will not be match against when using the rule (as if they were replaced by unapplied fresh variables).

**Remarks:**
- In order to make this feature type-safe,

Deduktichecks at runtime that the bracket constraint is verified whenever the rule may be used and fails otherwise. - This feature is not conditional rewriting. When a constraints is not satisfied, Dedukti doesn't just ignore the rule and proceed, it actually raises an error. - Because they are replaced with

Deduktican check the confluence of the rewrite system generated by the rewrite rules and beta-reduction, using an external confluence checker. For this you need to install a confluence checker for higher-order rewrite systems supporting the TPDB format, for instance CSI^HO or ACPH.

To enable confluence checking you need to call

dkcheckwith the option

-ccfollowed by the path to the confluence checker:

$ dkcheck -cc /path/to/csiho.sh examples/append.dk > File examples/append.dk was successfully checked.

A user can declare a symbol as private. A private symbol cannot be used outside the module it is defined. These symbols may freely occur in type annotation, definitions and rewrite rules within the file they are defined, however they are completely inaccessible to outside developments. Note that they may still appear in the normal forms or inferred types of terms that were defined without relying on them.

Deduktiis distributed under the CeCILL-B License.