Comment fusionner un ensemble de cartes finies?

Question

je peux fusionner deux cartes finies comme suit:

value "fmadd 
    (fmap_of_list [(1::nat,2::nat)]) 
    (fmap_of_list [(2::nat,3::nat)])" 

Mais lorsque je tente de fusionner un ensemble de cartes:

value "ffold fmadd fmempty {| 
    fmap_of_list [(1::nat,2::nat)], 
    fmap_of_list [(2::nat,3::nat)]|}" 

Je reçois l'erreur suivante:

Wellsortedness error: 
Type nat ⇀⇩f nat not of sort finite 
No type arity fmap :: finite 

Selon à la définition de fmap, son domaine est fini:

typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a ⇀ 'b) set" 
    morphisms fmlookup Abs_fmap 
proof 
    show "Map.empty ∈ {m. finite (dom m)}" 
    by auto 
qed 

Mais pourquoi fmap n'est pas fini?

Answer 1

Pour répondre à votre question immédiate:

But why fmap is not finite?

Chaque fmap a un domaine fini, mais il est pas nécessairement le cas où il n'y a que de nombreuses valeurs de finiment de type ('a, 'b) fmap. Par exemple, il existe une infinité de mappages de taille finie de nat à nat.

Le problème que vous observez est plus profond que cela: Je crois qu'il n'y a pas de configuration de code correcte pour ffold. Si j'essaie de calculer

ffold funion fempty {| 
    fset_of_list [(1::nat,2::nat)], 
    fset_of_list [(2::nat,3::nat)]|} 

... le message d'erreur est similaire. Pour l'instant, je recommande la réécriture comme fold sur les listes:

fold fmadd [ 
    fmap_of_list [(1::nat,2::nat)], 
    fmap_of_list [(2::nat,3::nat)]] fmempty 

Ce n'est pas la même chose, mais il serait peut-être utile pour votre application.