When you run Bedwyr, you specify a list of definition files, which contain objects to be declared and defined. You can then use the toplevel to ask queries against those definitions.
There is also a special brand of commands, meta-commands, which can appear anywhere.
As a general rule, any kind of input ends with a full-stop. Commands start with uppercase letters, meta-commands with hashes, and queries are just formulae.
Definition files are usually named with a
.def extension. You
can find several of them in the examples/ directory of the Bedwyr
distribution. They contain declarations for types
Kind <id> type.), declarations for constants
Type <id> type.), declarations and definitions for
Define <id> : <type> by <definitions>.), and
Theorem <id> : <formula>.).
The only meta-command that is really intended for definition files is
the include command:
#include "another/file.def". This can
really be seen as the plain inclusion of another file, as Bedwyr doesn’t
have any namespace or module system. If the path is not absolute, it is
relative to the path of the current file, or the execution path for the
Assuming Bedwyr is installed in standard Linux system folders, you can use the Emacs mode for Bedwyr by adding these two lines to your /.emacs file:
(load "/usr/share/bedwyr/contrib/emacs/bedwyr.el") (setq bedwyr-program "/usr/bin/bedwyr") ;; Of course you can change both locations to wherever you want.
Then you should be able to load any
.def file and have syntax
highlighting and some rough auto-indenting. Also if you do
C-c C-c it will start Bedwyr and load the current file you are
There is also a basic syntax highlighting file for Vim. With a standard system installation, the files /usr/share/vim/vimfiles/[ftdetect|syntax]/bedwyr.vim should suffice; otherwise do the following:
The interactive toplevel is automatically launched once the files have
been parsed, unless the flag
-I is passed to Bedwyr. In it, you
can either query a formula, or run a meta-command. In queries, free and
bound variables are the only objects that can be used without prior
declaration, and the solutions are displayed as instantiations of free
Queries can also be given in batch mode, to a non-interactive toplevel,
via the command-line option
bedwyr -e 'X = 0.').
In this case, they are processed after the files and before the
In 1 we load a set of definitions and prove (twice) that the untyped λ-term λ x.x x has no simple type.
Notice that we had to use the term
(abs x\ app x x) instead
(x1\ x1 x1): the former encodes the untyped
λ-term λ x.x x by mapping object-level abstraction to
abs and object-level application to
the latter would map them directly to logic-level abstraction and
application, and therefore is not a legal term in Bedwyr. (Prior to
version 1.3, this was allowed as Bedwyr did not use simple typing on its
Most of the errors that can stop the reading of a file (parsing or typing error, undeclared object, etc.) are correctly caught by the toplevel, though the line number reported for the error is often not useful.
Bedwyr has no line editing facilities at all. Thus, we recommend using
rlwrap, which provides such features. Get one
of them from your usual package manager or at
Then you can simply run
ledit bedwyr. One can also define an
alias in his /.bashrc, such as the following which also makes use
of /.bedwyr_history to remember history from one session to
alias bedwyr="ledit -h ~/.bedwyr_history -x /path/to/bedwyr"
Meta-commands are used to change the state or the program, or for non-logical tasks. They can be used any time a command or query is allowed.
Those commands alter the set of definitions the current session of
Bedwyr holds. An empty session actually means that only pervasive
types, constants and predicates are known. The session’s initial state
is the list of files given on the command-line, and it can grow anytime
with the use of
#include. It should be noted that, although
Bedwyr has no solid notion of what a module is, it tries to do the smart
thing by ignoring the request to include a file if it appears to be
already loaded in the current session, as failure to do this would
result in fatal multiple declarations. This only works if the same path
is used for each inclusion; for instance, ./file.def and
file.def will be seen as different files.
.deffile to the current session. It is designed to be used in definition files.
#sessionis an advanced
#includemeant for query mode. It accepts any number of filenames as parameters, and this set of files will be remembered as the new session. When you pass filenames on Bedwyr’s command line, it is equivalent to a call to
#sessionwith these definition files.
#reloadclears all the definitions, and then reloads the session’s initial state, i.e. the definition files given on the command-line. It is useful if they have been changed.
#resetclears all the definitions and empties the session. It is synonymous to
#sessionwith no arguments.
Three kinds of assertions can be used in definition files. These tests
are not executed unless the
-t flag has been passed on Bedwyr’s
command-line, in which case any assertion failure is fatal.
#assertchecks that a formula has at least one solution.
#assert_notchecks that a formula has no solution.
#assert_raisechecks that the proof-search for a formula triggers a runtime error.
Our examples include a lot of assertions, to make sure that definitions
have (and keep) the intended meaning. These assertions are also the
basis of Bedwyr’s correctness and performance tests ran using
#envdisplays the current session (types, constants and predicates).
#typeofdisplays the (monomorphic) type of a formula and of its free variables.
#show_defdisplays the definition of a predicate.
#show_tabledisplays the content of the table of an inductive of co-inductive predicate.
#save_tablewrites the table of an inductive of co-inductive predicate in a fresh definition file.
#exportexports a structured aggregate of all tables in a file. This functionality has to be enabled at compile-time.
#equivariantenables an alternative tabling mode.
#clear_tableclears the results cached for a predicate.
#clear_tablesclears all cached results.
#freezingsets the depth of backward-chaining during proof-search.
#saturationsets the depth of forward-chaining during proof-search.
#debugadds a lot of output during the proof search.
#timedisplays computation times between two results.
#helpis what you should type first.
#exitis what you should type last.