WEKO3
アイテム
Agda による Zorn の補題の証明
https://ipsj.ixsq.nii.ac.jp/records/232294
https://ipsj.ixsq.nii.ac.jp/records/23229455d0fe69-23ec-46bf-95e9-b0846885fe5c
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WPRO2023004.pdf (265.0 kB)
|
Copyright (c) 2023 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2023-01-06 | |||||||
| タイトル | ||||||||
| タイトル | Agda による Zorn の補題の証明 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | A Proof of Zorn Lemma in Agda | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | Agda Set-Theory Proof | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
| 資源タイプ | conference paper | |||||||
| 著者所属 | ||||||||
| 琉球大学工学部 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Faculty of Engineering, University of the Ryukyus | ||||||||
| 著者名 |
河野, 真治
× 河野, 真治
|
|||||||
| 著者名(英) |
Shinji, KONO
× Shinji, KONO
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 集合論は数学では古典的な基礎なので避けて通れない。Agda は Curry Howward 対応で証明を記述できる純関数型言語である。Agda 向きの集合論の公理を提案し、その有用性示すの例題として Zorn の補題の証明を行った。Zorn の補題はチコノフの定理などに使われる重要な定理であり、それを証明付きデータ構造を用いてAgdaで証明する。直観主義論理での集合論について考察する。 | |||||||
| 書誌情報 |
第64回プログラミング・シンポジウム予稿集 巻 2023, p. 5-16, 発行日 2023-01-06 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
