dedukti-1.1.2: doc/manual.texi.in

\input texinfo
@setfilename dedukti.info
@macro dkversion
esyscmd(awk '/^version:/{print $2}' ../dedukti.cabal)dnl
@end macro
@settitle Dedukti User's Guide, version @dkversion{}
@documentencoding UTF-8
@afourpaper

@copying
Copyright @copyright{} 2009 CNRS - École Polytechnique - INRIA.

@quotation
Permission is granted to copy, distribute and/or modify this document
under the terms of the GNU Free Documentation License, Version 1.3 or
any later version published by the Free Software Foundation; with no
Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A
copy of the license is included in the section entitled ``Copying this
manual''.
@end quotation
@end copying

@iftex
@macro lambdapi
@tex
$\\lambda\\Pi$%
@end tex
@end macro
@end iftex
@ifnottex
@macro lambdapi
λΠ
@end macro
@end ifnottex

@defindex df

@macro dindex {entry}
@dfindex \entry\
@end macro

@macro oindex {entry}
@dfindex Operator, @code{\entry\}
@end macro

@synindex df cp
@syncodeindex fn cp

@titlepage
@title Dedukti User's Guide
@subtitle Version @dkversion{}
@author Mathieu Boespflug (@email{mboes@@lix.polytechnique.fr})
@page
@vskip 0pt plus 1filll
@insertcopying
@end titlepage

@contents

@node Top
@top The Dedukti proof checker

This is the manual for Dedukti, version @dkversion{}. Dedukti is a proof checker
for the @lambdapi{}-calculus modulo.

@menu
* Overview::            The general architecture.
* Installation::        How to install the Dedukti system.
* Dedukti syntax::      The input language for Dedukti.
* Invoking dedukti::    The compiler.
* Invoking dkrun::      Executing the proof checks.
* References::          Bibliographic references.
* Copying this manual:: How you can copy and share this manual.
* Index::
@end menu

@node Overview
@chapter Overview
@cindex architecture
@cindex overview
@cindex general usage

@cindex @lambdapi{}-calculus modulo
The @lambdapi{}-calculus is a dependently typed lambda-calculus that
allows expressing proofs of minimal predicate logic through the
Brouwer-Heyting-Kolmogorov interpretation and the Curry-de Bruijn-Howard
correspondence. It can be extended in several ways to express proofs of
some theory. One way is to express the theory in Deduction modulo, i.e.
to orient the axioms as rewrite rules and to extend the
@lambdapi{}-calculus to express proofs in Deduction modulo. We get in
this way the @dfn{@lambdapi{}-calculus modulo}.

Dedukti is a type checker for the @lambdapi{}-calculus modulo.

The input is a series of source files that declare terms and define
rules. Checking these declarations with respect to the given rules is a
two step process. These source files are first compiled to object files.
The objects files for each source file are then linked together before
being executed to type check the rules and declarations of the input.

As such the Dedukti system centers around two commands. @command{dedukti}
is the compiler that generates object files from source files
(@pxref{Invoking dedukti}). @command{dkrun} is the command that links all
object files together and executes the resulting program
(@pxref{Invoking dkrun}).

@node Installation
@chapter Installation
@cindex configure
@cindex setup
@cindex install

@cindex Cabal
@cindex Hackage
Dedukti uses the Cabal architecture for building and packaging
applications and libraries. Regardless of the method of installation
chosen, one needs to satisfy manually dependency on system libraries,
such as the PCRE library. It might also be necessary to install
development version of these packages, depending on your distribution.

@menu
* Requirements::        Required versions for compiler and libraries.
* Local install::       Installing in your home directory.
* Global install::      Installing in the system directories.
* Building the documentation::     How to build the documentation.
* Smoke tests::         Running smoke tests (for developers)
@end menu

@node Requirements
@section Requirements
@cindex system libaries
@cindex Haskell compiler

Dedukti requires the Glorious Haskell Compiler (GHC) versions 6.10 and
above to compile. Note that GHC 6.12.1 has a bug preventing a dependency
of Dedukti to compile properly, so ulterior revisions in the 6.12 series
are recommended.

The PCRE library version 7.0 or above, including the header files, must
be present on the system before proceeding to @ref{Local install} or
@ref{Global install}. Dedukti has an indirect dependency on @code{happy
>= 1.17}. You should ensure that the @command{happy} command is in a
location mentioned in your @env{PATH}.

@node Local install
@section Installing Dedukti locally

If you have the @command{cabal} command part of the @code{cabal-install}
package, then you can obtain Dedukti from Hackage, configure and install
it all in one go:

@example
$ cabal install dedukti --user
@end example

@cindex Haskell Platform
@noindent
@code{cabal-install} is shipped as part of the Haskell
Platform@footnote{@uref{http://hackage.haskell.org/platform}}.
Alternatively, unpack the Dedukti source tarball and run

@example
$ cabal configure --user
$ cabal build
$ cabal install
@end example

You will have to satisfy dependencies by hand, if necessary. This will
install the Dedukti commands and other files under the Cabal hierarchy in
your home directory (typically @file{~/.cabal}). You will need to alter
your @env{PATH} appropriately to run these commands.

@node Global install
@section Installing Dedukti globally

If you have appropriate permissions, you can install Dedukti globally for
all users of the system. If you have the @command{cabal} command then
you can obtain Dedukti from Hackage, configure and install it all in one
go:

@example
$ cabal install dedukti --global
@end example

@noindent
Alternatively, unpack the Dedukti source tarball and run

@example
$ cabal configure --global
$ cabal build
$ cabal install
@end example

@node Building the documentation
@section Building the documentation

If you prefer to have a local copy of this documentation, you can build
it from the @file{doc/} folder in the source distribution. The build
system is based on an @file{mkfile}, which plays the same role as
@command{make}'s @file{Makefile} but with a slightly different syntax
and simpler semantics. You can interpret @file{mkfile}'s using either
Plan 9's original mk
command@footnote{@uref{http://plan9.bell-labs.com/magic/man2html/1/mk}},
or by using @command{hmk}, a Haskell clone of @command{mk} which is a
dependency of Dedukti.

To build the pdf version of this manual:

@example
$ cd doc
$ hmk pdf
@end example

@noindent
To build the html version of this manual:

@example
$ cd doc
$ hmk html
@end example

The @command{hmk} command is part of the @file{hmk} Cabal package. It
may be found either somewhere in your global path, or in Cabal's user
folder, depending on the type of installation. You will also need a
POSIX compatible environment to build the documentation, including the
@command{m4} command to preprocess the texinfo source.

@node Smoke tests
@section Smoke tests
@cindex test harness
@cindex smoke tests

The package description file for Dedukti declares a @code{test} flag.
Enabling this flag instructs Cabal to build the test harness as well.
The test harness currently contains a handful of smoke tests useful for
sanity checking of new patches to Dedukti, for instance.

In a Dedukti source directory, one can perform smoke tests as follows:

@example
$ cabal configure -f test
$ cabal build
$ cabal test
@end example

New changesets should not be submitted unless all tests pass.

@node Dedukti syntax
@chapter Dedukti syntax

@menu
* Syntax overview::         An informal description of input files.
* Pragmas::                 Use source pragmas for compiler hints.
* Scoping rules::           The scope of declarations and rules.
* Grammar::                 A formal specification of the syntax.
* Prefix notation grammar:: A formal specification of an alternative syntax.
@end menu

@node Syntax overview
@section A informal overview of the syntax

@dindex module
@cindex top-level
@cindex source file
A Dedukti source file consists in a series of top-level declarations
rules, all terminated by a period. Each source file defines a
@dfn{module}.

@subsection Declarations

Declarations have the form

@example
t : A.
@end example

@noindent
where @code{t} is an identifier and @code{A} is a type.

@anchor{Rules}
@subsection Rules

@cindex rule environment
@cindex pattern
@dindex rule
@dindex rule head
@dindex head, of a rule
@cindex head constant
@oindex -->
Rules always start with an environment, followed by a head on the left
hand side and an expression on the right hand side of a long arrow. A
@dfn{rule head} consists of a head constant and zero or more patterns.
Here is an example:

@example
S : nat.
O : nat.
[y : nat] plus O y --> y.
[x : nat, y : nat] plus (S x) y --> S (plus x y).
@end example

@noindent
Two rules, each with two patterns in the head, are defined for the
constant @code{plus}. All variables in the pattern must appear in the
environment along with a type. All identifiers that are not mentioned in
the environment are considered constants, which must be in scope of
their declaration (@pxref{Scoping rules}). Here @code{O} and @code{S}
are constants declared earlier. The free variables in the right hand
side of the rule must be a subset of the pattern variables mentioned in
the left hand side. It is illegal to put variables in the rule
environment that are not also pattern variables in the left hand side of
the rule.

A current limitation of the implementation imposes that rules for the
same head constant be defined contiguously and in the same module as the
declaration of the head constant. Another limitation is that all rules
must have same arity. That is, the head constant in each rule must be
followed by the same number of patterns. Both limitations may be lifted
in the future.

@subsection Terms and types
@cindex term
@cindex sort
@cindex product
@cindex dependent product
@cindex variable

@dindex term
@dindex type
@dindex dependent product
@dindex product
@dindex abstraction
@findex Type
@findex Kind
As in many dependently-typed languages, the @lambdapi{}-calculus modulo
unifies the syntax of terms and types. Nearly all terms have types and
those types are themselves terms. There are two special terms,
@code{Type} and @code{Kind}, which we refer to as @dfn{sorts}. In the
following, we will call @dfn{types} those terms whose type is a sort.

A term is either a variable, an application of terms, and abstraction of
a variable over a term, a dependent product or a sort.
@dfn{Abstractions} are the regular lambda-abstractions of the
lambda-calculus with an extra type annotation on the bound variable. It
is written in Dedukti as in the following example:

@oindex =>
@example
x : A => t
@end example

@noindent
where @code{x} is a variable, @code{A} is a type and @code{t} is a term.
Parentheses around the abstraction are optional. A product is written
similarly:

@oindex ->
@example
x : A -> B
@end example

@noindent
with @code{A} and @code{B} types. As a convenience, if the variable
@code{x} does not appear free in the type @code{B}, one may write

@example
A -> B
@end example

@dindex application
@noindent
instead. Finally @dfn{applications} are written as a simple
juxtaposition of terms, as in @code{t1 t2}.

@cindex operator precedence
@cindex precedence
@cindex associativity
@quotation Note
Products bind more strongly than abstractions, so that @code{x : A -> B
=> t} is parsed as @code{x : (A -> B) => t}. Also, applications are
left-associative, while products are right-associative. This means that

@example
((a b) c) d -> (e (f g) -> h)
@end example

@noindent
is equivalent to

@example
a b c d -> e (f g) -> h
@end example
@end quotation

@node Pragmas
@section Pragmas
@cindex pragmas

Multi-line comments whose first non-blank character following the
comment delimiter is a hash ``@verb{.#.}'' symbol are treated specially
by Dedukti. These comments are considered @dfn{pragmas}, providing hints
to the compilation process. The syntax of pragmas is as follows.
Following the hash sign is the name of the pragma, in upper case. All
remaining tokens until the closing comment delimiter are arguments to
the pragma.

Currently, the only supported pragma is the @code{FORMAT} pragma,
expliciting the syntax of the source file in which it occurs. This
pragma may only appear on the first line of the source file, as in the
following:

@example
(; # FORMAT prefix ;)
@end example

This line says that the source file is in prefix notation (@pxref{Prefix
syntax}).

@node Scoping rules
@section Scoping rules
@cindex scoping
@cindex lexical scoping
@cindex rules, scope of
@cindex axioms, scope of

An axiom declaration introduces the axiom into scope from the end of the
declaration to the end of the file. Binding constructs such as products
and abstractions introduce new variables whose scope encompasses the
entire binding construct, i.e.@: variables are lexically scoped.

Rules may be defined anywhere within the scope of the head constant to
which it pertains and the scope of the constants appearing in the left
and right hand sides of the rule. As noted in @ref{Rules}, rules must be
defined in the same module as the declaration of the head constant.

@node Grammar
@section The grammar of axioms and rules
@cindex grammar
@cindex syntax

The concrete syntax for the @lambdapi{}-calculus modulo used by Dedukti
is given by the following grammar.

@example
qid ::= id.id | id
toplevel ::= declaration toplevel
           | rule toplevel
           | eof
binding ::= id ":" term
declaration ::= binding "."
domain ::= id ":" applicative
         | applicative
sort ::= "Type"
term ::= domain "->" term
       | domain "=>" term
       | applicative
simple ::= sort
         | qid
         | "(" term ")"
applicative ::= simple
              | applicative simple
rule ::= env term "-->" term "."
env ::= "[]"
      | "[" env2 "]"
env2 ::= binding
       | binding "," env2
@end example

@node Prefix notation grammar
@section Axioms and rules in prefix notation
@cindex grammar
@cindex syntax
@cindex prefix notation
@cindex polish notation

For the rationale behind prefix notation, see @ref{Prefix syntax}

Source files in prefix notation consist in a string of whitespace
delimited tokens, as is the case for the human-readable format defined
above. Unlike that format, however, there is no syntax for comments,
though a @code{FORMAT} pragma may appear on the first line. Any token
that is not one of the literals appearing in the grammar below is
considered an identifier. Identifiers are period separated lists of
characters, everything before the last period specifying the module
qualifier for an identifier.

@example
qid ::= id.id | id
toplevel ::= binding toplevel
           | rule toplevel
           | eof
binding ::= ":" id term
sort ::= "Type"
term ::= "->" binding term
       | "=>" binding term
       | "@@" term term
       | qid
rule ::= "-->" env term term
env ::= "[]"
      | "," binding env
@end example

@node Invoking dedukti
@chapter Invoking @command{dedukti}

@menu
* One-shot mode::       Compiling one source file at a time.
* Batch mode::          Let Dedukti figure out what needs to be compiled.
* Prefix syntax::       Input source files to Dedukti in alternative syntax.
@end menu

@node One-shot mode
@section One-shot mode

The simplest mode of operation is the one-shot mode. @command{dedukti}
will create a @file{.dko} file from the given source file. If the source
file refers to other modules, then compilation may only proceed if the
source files for those modules have also been compiled beforehand.

A source file @file{a.dk} can be compiled as follows:

@example
$ dedukti a.dk
@end example

@noindent
Once a @file{.dko} file has been produced, one can further process this
file in order to obtain native object code. The @file{.dko} file is in
fact Haskell source code, so it can be compiled using the GHC Haskell
compiler. If this step is omitted, then the @file{.dko} file will be
converted to bytecode on the fly by @command{dkrun} when it is loaded.
Hence for better performance, it is better to compile all @file{.dko}
files with the GHC compiler, so that native code will be used when
checking each module, rather than bytecode. To have GHC called
automatically for you with the right flags, see @ref{Batch mode}.

The @file{.dk} extension may be omitted. If @file{a.dk} mentions modules
@code{b} and @code{c} then files @file{b.dk} and @file{c.dk} need to be
compiled first. The next section details how to have @command{dedukti}
figure out dependencies and compile them in the right order
automatically.

@node Batch mode
@section Batch mode

Compile in batch mode by passing the @code{--make} option to
@command{dedukti}. In this mode, dependencies of the file given in
argument will be compiled first, though after the dependencies of the
dependencies have been compiled, etc. Those dependencies that do not
need rebuilding, because their object file is up to date with respect to
the source file, will not be rebuilt.

In addition, calling @command{dedukti} in batch mode will cause it to
invoke GHC on all compiled files, so as to produce native object code
for the module given as argument and its dependencies. Compiling to
native code often yields much better performance during checking.
@xref{Invoking dkrun}.

@node Prefix syntax
@section Prefix syntax
@cindex prefix notation
@cindex polish notation
@cindex syntax
@cindex source files
@cindex parsing

Because Dedukti may be used as the backend proof checker for a number of
frontend mechanized translators, proof assistants and other interactive
environments, in many cases the input to Dedukti is not human crafted
but mechanically generated. Dedukti therefore accepts source files in an
alternative syntax that can be parsed much more efficiently, inspired by
Jan Łukasiewicz' polish notation for sentential
logic@footnote{@uref{http://en.wikipedia.org/wiki/Polish_notation}}. The
syntax uses prefix notation for operators, much like Lisp, but unlike
Lisp, arities for all the operators are fixed and known in advance,
therefore no parentheses are need around subterms.

This syntax for Dedukti axioms and rules is the preferred target syntax
for automated tools that produce Dedukti code. Parsing time is at least
an order of magnitude smaller for source files in prefix notation.
Dedukti can automatically recognize the syntax of the source file if the
first line of the source file is a @code{FORMAT} pragma
(@pxref{Pragmas}). It is also possible to force a particular format
using the following command line options:

@table @option
@item -fexternal
Force recognizing input as (human-readable) external format.

@item -fprefix-notation
Force recognizing input as (fast) prefix format.

@end table

See @ref{Prefix notation grammar} for the lexical and grammatical
structure of this syntax.

@node Invoking dkrun
@chapter Invoking @command{dkrun}

@command{dkrun} is a wrapper script@footnote{It can be found in the
source distribution of dedukti or under the data directory of Cabal.
Copy it somewhere in your path for convenience.} that invokes
@command{ghci} with the appropriate flags on the Haskell source files
(@file{.dko} files) given as arguments. If object files exist for the
given @file{.dko} files, then these are loaded into memory and linked by
the @command{ghci} linker. Otherwise the files are compiled to slower,
interpreted bytecode by @command{ghci}.

The first argument to @command{dkrun} is the @file{.dko} file
corresponding to the module one wants to proof check. If a module has
dependencies, then the Haskell source files corresponding to these
dependencies must be given as additional arguments to
@command{dkrun}@footnote{This is a limitation of the current
implementation and may be lifted at some point in the future.}. Say
@code{A} depends on @code{B} and @code{C}, @code{B} depends on @code{D}.
Then the following command proof checks @code{A}:

@example
$ dkrun A.dko B.dko C.dko D.dko
@end example


@node References
@chapter References

@enumerate

@include references.texi

@end enumerate

@ifnottex
@node Copying this manual
@appendix Copying this manual

@include fdl.texi
@end ifnottex

@node Index
@unnumbered Index

@printindex cp

@bye