Re: [isabelle] Method sos fails depending on variable names



On 01/02/18 00:32, Dominique Unruh wrote:
> 
>     As supposed, there is a mismatch in term orderings, one sorting
>     first by string length, the other lexicographically.
>     Looking at term_ord.ML, the first would be fast_term_ord, and the
>     second term_ord.
> 
>     Of course, without understanding the code, we cannot be sure that
>     this is exactly what's needed. In particular, there are also calls
>     to FuncUtil.cterm_ord (which internally uses fast_term_ord). Should
>     they be replaced, too? It does not seem to make a difference for my
>     test case, but who knows. In any case, I think replacing
>     fast_term_ord in the two places is better than the status quo.

The Isabelle/ML library provides various ways to order terms, and some
other more basic data types like string and indexname.

Working with the Simplifier (or related conversions) usually requires an
ordering that conforms to its policies, notably Term_Ord.term_ord /
termless (sometimes Term_Ord.term_lpo).

Working with auxiliary set/map data structures that need to be fast is
usually done with fast_string_ord, fast_indexname_ord, fast_term_ord
etc. There is no semantic intention behind these orderings, and they can
actually look strange when used for printing a table: the output needs
to be sorted by a more natural order.


With this in mind an educated guess says: FuncUtil tables are right in
using fast_term_ord derivatives and sum_of_squares.ML was wrong using
fast_term_ord with Semiring_Normalizer. This is further supported by the
empiric exploration of Isabelle + AFP: the change c46910a6bfce was
sufficient to make the counter examples work and did not break existing
applications.

There is additional confusion in this code base due to preference of
cterm over term: it might be a consequence of porting tools from
HOL-Light, which only has cterm (and calls it term). There are also a
bit too many clones of operations, with non-canonical name and signature
(like simple_cterm_ord, which corresponds to Term_Ord.termless).


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.