1

で最初の実験を行っていますcodatatypeが、かなり早く立ち往生しています。分岐する、おそらく無限のツリーのこの定義から始めました。

codatatype (lset: 'a) ltree = Node (lnext : "'a ⇒ 'a ltree option")

一部の定義は正常に機能します。

primcorec lempty :: "'a ltree"
  where "lnext lempty = (λ _ . None)"

primcorec single :: "'a ⇒ 'a ltree"
  where "lnext (single x) = (λ _ . None)(x := Some lempty)"

しかし、これは機能しません:

primcorec many :: "'a ⇒ 'a ltree"
  where "lnext (many x) = (λ _ . None)(x := Some (many x))"

エラーメッセージが表示されるので

primcorec error:
  Invalid map function in "[x ↦ many x]"

私は書くことでそれを回避することができました

primcorec many :: "'a ⇒ 'a ltree"
  where "lnext (many x) = (λ x'. if x' = x then Some (many x) else None)"

これは、 が補題を必要とし、補題が必要primcorecであるのと同様に、関数更新演算子について「何かを知る」必要があると思わせます。しかし、正確には何ですか？funfundef_conginductivemono

4

1 に答える 1

2

codatatype が他の型コンストラクターを介しprimcorecて再帰する場合、再帰呼び出しがこれらの型コンストラクターのマップ関数で適切にネストされていることが期待されます。この例では、再帰は関数型とオプション型を通過します。そのマップ関数はop oとmap_optionです。したがって、 への再帰呼び出しmanyは の形式にする必要がありますop o (map_option many)。したがって、次の定義が機能します。

primcorec many :: "'a ⇒ 'a ltree"
where "lnext (many x) = map_option many ∘ [x ↦ x]"

便宜上、primcorecさらにいくつかの構文入力形式をサポートします。特に、関数型のマップ関数は、ラムダ抽象化を使用して記述することもできます。さらに、大文字と小文字の区別とifs をサポートします。これが、2 番目のバージョンが受け入れられる理由です。ただし、生成された定義many_defを見ると、明示的なマップ関数よりも複雑であることがわかります。

primcorec任意の関数の登録には対応していないので、そのままでは使えませんfun_upd。プリミティブ共帰は構文的です。将来的には、 に対応するコアカーシブが存在する可能性がありますfunction。

マップ関数については、データ型に関するチュートリアルとこのペーパーで説明されています。

于 2014-11-12T10:26:25.727 に答える