repository·master·Indexed 42 days ago
https://github.com/deducteam/deduktiA type-checker for a rewrite-based calculus used for formal verification and theorem proving. It provides a logical framework for theories such as First-Order Logic (FOL), Calculus of Inductive Constructions (CiC), and Simple Type Theory (STT), and includes CLI tools like `dk check` for type-checking, `dk top` for interactive use, and `dk dep` for dependency generation.
The Dedukti libraries repository is organized into two main functional directories:
The libraries/paradoxes directory contains several formal encodings of logical and set-theoretic paradoxes using Deduction Modulo. These files serve as examples of how to represent inconsistent or paradoxical structures within the Dedukti framework.
Available paradox types include:
liar --> liar -> false) or non-circular variants like Yablo's paradox (yablo.dk, yablo2.dk).Type : Type) using constructions like $\Pi$, $\Sigma$, and $\mathbb{N}$.false in System $U^-$ (hurkens.dk).russell.dk), System $U^-$ pointed graphs (miquel.dk), and versions by Dowek and Werner (dowek_werner_russell.dk).The libraries/theories directory contains Dedukti encodings for several logical theories. Each theory is represented by a .dk file. These encodings allow Dedukti to act as a logical framework for different formal systems.
Available theories include:
fol.dk).cic.dk).opentheory.dk).stt.dk).sttforall.dk).A Dedukti file (typically with a .dk extension) must start with a #NAME line to define the module name. This name is used to reference the constants and functions defined in the file from other developments.
Module Declaration:
#NAME <module_name>. (e.g., #NAME foo.)
Comments:
Comments are enclosed by (; and ;).
In Emacs, you can insert them using M-;.
#NAME foo.
(; This is a comment ;Dedukti distinguishes between two types of symbol declarations:
f : A. These cannot be defined via rewrite rules.def f : A. These can be defined using rewrite rules.Nat: Type.
zero: Nat.
succ: Nat -> Nat.
def plus: Nat -> Nat -> Nat.
[ 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, Dedukti ensures they preserve typing by checking that the left-hand side (LHS) and right-hand side (RHS) have the same type in a valid context, and that the LHS is a higher-order pattern.
When a variable is not used on the right-hand side of a rewrite rule, you can replace it with an underscore _ on the left-hand side.
Example:
def mult : Nat -> Nat -> Nat.
[ n ] mult zero n --> zero
[ n, m ] mult (succ n) m --> plus m (mult n m).Can be written as:
[ ] mult zero _ --> zero.Note: In lambdas, _ => _ => z => zero is equivalent to x => y => z => zero. However, in a pattern, _ => _ means x => Y where both x and Y are fresh variables occurring nowhere else.
def mult : Nat -> Nat -> Nat.
[ ] mult zero _ --> zero.
[ n, m ] mult (succ n) m --> plus m (mult n m).Instead of manual evaluation, you can use Dedukti's type-checker to verify that a term reduces to a specific value. This is done by defining a dependent type (a family of types indexed by a value).
For example, to check if a boolean expression expr is True, define a type Istrue where tt is the only inhabitant of Istrue True:
Istrue : Bool -> Type.
tt : Istrue True.
-- This definition will only be accepted if 'expr' reduces to 'True'
def test1 : Istrue (expr) := tt.Istrue : Bool -> Type.
tt : Istrue True.
def test1 : Istrue (equal (mult 10 10) 100) := tt.A definition is syntactic sugar for a declaration followed by a rewrite rule.
def three : Nat := succ ( succ ( succ ( zero ) ) ). is equivalent to:
def three : Nat.
[ ] three --> succ ( succ ( succ ( zero ) ) ).Using thm instead of def makes a definition opaque. The symbol is declared, but the rewrite rule is not added to the system, meaning the symbol does not reduce to its body. This is useful when only the existence of a symbol matters.
thm three := succ ( succ ( succ ( zero ) ) ).def three : Nat := succ ( succ ( succ ( zero ) ) ).
// Equivalent to:
def three : Nat.
[ ] three --> succ ( succ ( succ ( zero ) ) ).
// Opaque version:
thm three := succ ( succ ( succ ( zero ) ) ).You can declare a symbol as injective to assist the type checker. Dedukti does not perform an injectivity check itself; it simply assumes the symbol is injective when type-checking subsequent rules.
Warning: Declaring a non-injective symbol as injective can break the injectivity of products and subjection reduction.
injective double : Nat -> Nat.
[ ] double zero --> zero.
[ n ] double (succ n) --> succ (succ (double n)).Bracket patterns allow you to mark parts of the LHS that are constrained by typing. Dedukti uses this information for typing but ignores it during the actual matching process.
Example:
[ n, v1, m, e, v2 ] append (succ n) (cons {n} e v1) m v2 --> cons (plus n m) e (append n v1 m v2).A smart constructor is a symbol (like a constructor) that has rewrite rules applied to it. This allows you to define types where certain forms are automatically reduced to a canonical representation.
Example: Integers via Natural Numbers
By adding a rule to the Diff constructor, we can ensure that Diff (S m) (S n) always reduces to Diff m n:
Int : Type.
def Diff : Nat -> Nat -> Int.
[m,n] Diff (S m) (S n) --> Diff m n.This ensures that the only irreducible (normal) forms for Int are Diff 0 0, Diff (S n) 0, and Diff 0 (S n).
Int : Type.
def Diff : Nat -> Nat -> Int.
[m,n] Diff (S m) (S n) --> Diff m n.make command. Note that running the full suite of examples is expected to take approximately 8 minutes.make