Re: [isabelle] Non-idempotence of datatype constructors



Hi Manuel,

> On 4 May 2020, at 17:06, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> On 03/05/2020 11:46, Traytel Dmitriy wrote:
>> while your code works for the examples you show, it does not seem to handle nested recursion.
> 
> Yes, I am aware of that. Nested datatypes make things considerably more
> complicated, so I'd rather not support that for now. I'd have to
> 1. somehow figure out /all/ the other datatypes involved in the
> definition of my datatype and
> 2. figure out a robust way to expand their size functions.
> 
> I have no idea how to do 1 with the information provided by the BNF
> package (other than inspecting the types of the constructors to figure
> out the nesting).

We store the BNFs that nest recursive occurrences in fp_nesting_bnfs (in fp_sugar). There is also the live_nesting_bnfs for BNFs that nest an occurrence of one of the datatype's (live) type variables. See the following examples:

datatype 'a tree = Node 'a "'a tree list"
datatype ('a, 'b) tree2 = Node "'b ⇒ 'a option" "(('a, 'b) tree2 list × 'a) tree"
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name list} |> the |> #fp_nesting_bnfs›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree} |> the |> #fp_nesting_bnfs |> map BNF_Def.name_of_bnf›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree} |> the |> #live_nesting_bnfs |> map BNF_Def.name_of_bnf›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree2} |> the |> #fp_nesting_bnfs |> map BNF_Def.name_of_bnf›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree2} |> the |> #live_nesting_bnfs |> map BNF_Def.name_of_bnf›

I'm not 100% sure whether you only need the fp_nesting_bnfs or the union of the two. And of course you will need the associated fp_sugars rather than just BNFs (for those types that are in fact datatypes), but these are easy to get once you have the names.

> I also have no idea how to do 2 properly – the "size" plugin provides
> some information with BNF_LFP_Size.size_of, but oddly enough it only
> provides the equations for the "regular" size function "size", but not
> for the generalised one (e.g. "size_list"), which appear in the size
> functions of nested datatypes.

Jasmin can say more but it is probably due to the fact that the old interface didn't provide the generalized equations either. You could access the equations by name (cf. "List.list.size"), but this is of course a bit fragile. The correct way would be to extend BNF_LFP_Size's interface. The equations should be available internally.

> Note that I really do want to do 2, because relying on the simplifier
> itself to solve the precondition "size lhs ≠ size rhs" is fragile and
> breaks at least in some cases in the AFP.

Makes sense.

>> I am sympathetic to the proposal of having a 'proper
>> subexpression' ordering defined for
>> all datatypes (e.g., via a plugin similarly to size).
>> Its usefulness goes beyond the
>> acyclicity rules which this thread is about.
> 
> Absolutely! It's probably no surprise to you when I say that I won't
> implement this. But if you (or one of our other datatype experts) ever
> does it, do let me know!

I won't promise anything, but will keep this in mind for students looking for theses. :)

>> But one would like to have some reasonable simp rules for subexp_x
>> (which may be as hard as the original problem that you are trying to solve). 
>> In particular, if F is itself a datatype that belongs to the subexp type class, 
>> its notion of subexp should be linked to the one of x.
> 
> Already for mutual and nested datatypes, you would probably need an
> entire family of relations for each combination of types (e.g. if you
> have mutually recursive datatypes A and B, you would probably need
> subexpr_A_A, subexpr_A_B, subexpr_B_A, subexpr_B_B).

Right, or just one subexpr_(A+B)_(A+B) which is reminiscent of what function does for mutual recursion.

> I guess everything gets complicated once you involve nested datatypes…

Actually, no. Because nesting is handled by the virtue of BNFs (more precisely their set function) in this case. See my example, where the recursive occurrence of x was nested in F.

Dmitriy



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