[Termtools] (sub) categories, specification of input format, test cases

[Rene Thiemann]

Dear all,

> The input format http://www.lri.fr/~marche/tpdb/format.html
> is semantically underspecified in several places, e. g.
> what happens for "(STRATEGY INNERMOST) (STRATEGY OUTERMOST) ..."
> what theories are pre-defined (A, C, AC  I guess)?
> what is "(THEORY (A x) (C x))", do these declarations accumulate?

just another one:

What is the semantics of underspecified symbols in context-sensitive rewriting 
as in the following example. (there are several new examples in TPDB which 
are underspecified) 

(STRATEGY CONTEXTSENSITIVE
(f 1)
)
(RULES
f(a) -> g(f(a))
)

The replacement map can only be determined for f and a (constants always have 
the empty replacement map). But what about g?

We should either disallow such a CSR and correct all of these examples in the 
TPDB or fix mu(g) = emptyset or mu(g) = {1..arity(g)} for all non-specified 
symbols g.

What do you think?

Best regards,
Rene
-- 
René Thiemann         mailto:thiemann at informatik.rwth-aachen.de
LuFG Informatik II    http://www-i2.informatik.rwth-aachen.de/thiemann
RWTH Aachen           phone: +49 241 80-21241

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools