リストのconsの型をA -> list A -> list AではなくA -> list (list A) -> list Aにした型をHaskellとCoq/SSReflectで定義したい - Qiita
リストのconsの型をA -> list A -> list AではなくA -> list (list A) -> list Aにした型をHaskellとCoq/SSReflectで定義したいHaskellCoqssreflectリスト形式検証 はじめに 本記事はTPP2024で発表した内容になります。 リストlistの型は通常nilとconsの2つのコンストラクタから定義されますが、 型変数Aに対し、cons A型をA -> list A -> list AではなくA -> list (list A) -> list Aに変更した型をHaskellやCoq/SSreflectで定義する方法について記述します。 ソースはこちら Haskellで定義する まず、この型の名前をSSeqとしてHaskellで実装したものは以下のようになります。
クイックソートは半順序でもソート可能であることをCoq/SSReflectで証明する - Qiita
はじめに 前回の記事で、全順序が仮定されているからこそうまくいくソートアルゴリズムを半順序で使用するとどうなるかを見ました。結果としてクイックソートなら半順序でもうまくソートできることを見ましたが、本記事では、これを定理証明支援系Coqを用いて、形式的に証明していきます。 定理証明支援系Coqに関して軽く説明しておくと、プログラムが正しく動くことを、数学的に検証できるツールとして使えるものです。 クイックソートを定義 SSReflectのpathライブラリには、標準のソート関数sortが定義されていますが、このアルゴリズムはマージソートなので、前回の記事で検証したように半順序では使えません。 そこでCoqでクイックソートを定義します。 まず定義の前に、ソートを行う要素の集合Tと、半順序関係Rを宣言しておきます。実際にはTは型で、RはただのT上の二項関係T -> T -> boolとして定義
半順序でソートするためのアルゴリズムとは？ - Qiita
Deleted articles cannot be recovered. Draft of this article would be also deleted. Are you sure you want to delete this article? はじめに ソートのアルゴリズムは通常、実数における通常の順序関係のように全順序である順序関係に対して行うものですが、本記事では半順序に対するソートのアルゴリズムについて解説します。 半順序とは 集合X上の二項関係 ≦ が半順序であるとは、以下の性質を満たすものとして定義されます。 反射律 任意のx $\in$ Xに対し、x ≦ x を満たす。 反対称律 任意のx, y $\in$ Xに対し、x ≦ y かつ y ≦ x ならば x = yを満たす。 推移律 任意のx, y, z $\in$ Xに対し、x ≦ y かつ y ≦ z ならば
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
