Re: [isabelle] BNFs and sort constraints



Hi Lars,

let me refine Jasmin's anwer.

> On 22 May 2018, at 21:57, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> 
> Hi Lars,
> 
>> Could somebody shed some light onto how this works? I looked at some of
>> the papers but didn't find anything.
> 
> I can answer Observation 4, which involves some of my code.
> 
> BNF type variables may not have sort constraints. "map_id" is part of the BNF structure, so it accordingly doesn't have sort constraints. More high-level theorems and constants are declared with the sort constraints. To overgeneralize a bit, Dmitriy's low-level BNF code doesn't like sort constraints, whereas my higher-level "(co)datatype" code copes with them to the extent possible. In the code, you'll see this by grepping for "unsorted_As" in "bnf_fp_def_sugar.ML".
> 
> I presume there's no deep reason for not supporting syntactic type class constraints in BNFs. It would complicate the composition operators for sure, and in a bunch of places we'd have to discharge 0 goals arising from syntactic type class instantiations. If you're up for putting in the effort, we won't stop you.


*Live* BNF type variables may not have sort constraints.

This is inherent: live variables indicate where we may recurse through. Imagine a BNF "'a :: foo F" with 'a live. Then we should be able to define:

datatype X = N | C "X F"

which in turn would require X to be an instance foo. Suddenly the datatype command would need to instantiate arbitrary type classes simultaneously with defining the type, which sounds quite ambitious even for syntactic type classes (e.g., one might get the "wrong" instance).

In contrast, *dead* BNF type variables may carry sort constraints. Consider e.g.,

datatype (dead 'a::plus, 'b) X = N 'b | C 'a "('a, 'b) X"
term map_X

where the first type argument of X in map_X has the sort constraint.

Sometimes one can even use the sort constraints on dead type variables to prove that some type is a BNF. My favorite example that uses this trick are arity-correct first-order terms:

declare [[typedef_overloaded]]

class arity =
 fixes arity :: "'a ⇒ nat"

instantiation unit :: arity begin
definition arity_unit :: "unit ⇒ nat" where "arity_unit x = 0"
instance proof qed

typedef (overloaded) ('c :: arity, 'ty) comb (infixr "$" 65) =
 "{(s :: 'c, Ts :: 'ty list). arity s = length Ts}"
 morphisms Rep_comb comb
 by (auto intro!: exI[of _ "replicate _ undefined"])

lift_bnf (no_warn_wits) (dead 'c :: arity, 'ty) comb by auto

setup_lifting type_definition_comb

lift_definition "fun" :: "'c :: arity $ 'ty ⇒ 'c" is fst .
lift_definition "args" :: "'c :: arity $ 'ty ⇒ 'ty list" is snd .

datatype ('x, 'c :: arity) "term" = Var 'x | App  "'c $ ('x, 'c) term"

Dmitriy

PS: For sure, copy_bnf should emit a proper failure instead of the tactic failure in "observation 1". I will have a look eventually.





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