Dedukti
Dedukti copied to clipboard
More pedagogical documentation
In the wake of the new documentation provided by #241, it can be further improved by
- explaining what the load path is,
- what happens when
--stdin
is used and a file is given as positional argument - document exit status
Some commands are not explained in README:
-
#REQUIRE
: is it mandatory? -
#NAME
: is it still accepted? -
defac
-
defacu
: what does that mean to declare a symbol ACU? -
#GDT
Indeed, contribution are welcome but in short:
-
#REQUIRE
is not mandatory but in some cases it is necessary (a rule in a file which depends on another rule, declared in another file to type check for example) - '#NAME' should not be accepted anymore
-
defac
is for anac
symbol -
defacu
is for anacu
symbol -
#GDT
is to print the decision tree of a symmbol
I welcome contributions with pleasure, but I don't have time to tackle all of this seriously for the moment, unfortunately.
But what ACU implies? Does that mean that matching is modulo ACU?
I suspect that if the top symbol of a rule (the symbol rewritten) is declared as ac
or acu
then we have matching (or filtering?) which is done ac
or acu
. I am not certain since I do not know that part of the code. Some description can be found here: https://github.com/Deducteam/Dedukti/pull/203
But what ACU implies? Does that mean that matching is modulo ACU?
More or less. I don't know what the exact definition of matching modulo ACU is, but the results of a small experiment tells us that one can match on the presence of the symbol, but not on the length of the list of its arguments (once flatenned), since matching modulo ACU allows to "invent" new application of the neutral element.
N : Type.
0 : N.
s : N -> N.
defacu plus [N, 0].
def f : N -> N.
[] f (plus _ _) --> 0.
#EVAL (f (s (s 0))). (; This line prints `f (s (s 0))` ;)
def g : N -> N.
[] g (plus _ (plus _ _)) --> 0.
#EVAL (g (plus (s (s 0)) (s 0))). (; This line prints 0` ;)
If one wants to see the "invented 0", modifying the last lines of the example gives us:
def g : N -> N.
h : N -> N -> N -> N.
[x,y,z] g (plus x (plus y z)) --> h x y z.
#EVAL (g (plus (s (s 0)) (s 0))). (; This line prints `h (s (s 0)) (s 0) 0` ;)