如何合併一組有限地圖？

Question

我可以合併兩個有限的地圖如下：

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

但是，當我嘗試合併組映射：

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

我收到以下錯誤：

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

根據定義爲fmap，它的域名是有限的：

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 

但是爲什麼fmap不是有限的？

Answer 1

要回答你的問題直接：

But why fmap is not finite?

每fmap具有有限的領域，但它不一定是隻有('a, 'b) fmap型的有限多值的情況。例如，從nat到nat有無限多的有限大小的映射。

您正在觀察的問題比這個更深：我相信ffold沒有正確的代碼設置。如果我嘗試計算

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

...錯誤消息是類似的。現在，我會建議重寫它作爲fold上列出：

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

這是不一樣的，但它可能是您的應用程序非常有用。