WEKO3
アイテム
Agda による Automaton の記述
https://ipsj.ixsq.nii.ac.jp/records/232282
https://ipsj.ixsq.nii.ac.jp/records/2322827aa65c9a-3666-4989-99e0-9772869e403b
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WPRO2024008.pdf (186.9 kB)
|
Copyright (c) 2024 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2024-01-06 | |||||||
| タイトル | ||||||||
| タイトル | Agda による Automaton の記述 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Automaon description in Agda | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | Agda, Automaton | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
| 資源タイプ | conference paper | |||||||
| 著者所属 | ||||||||
| 琉球大学工学部 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Faculty of Engineering, University of the Ryukyus | ||||||||
| 著者名 |
河野, 真治
× 河野, 真治
|
|||||||
| 著者名(英) |
Shinji, Kono
× Shinji, Kono
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | Automaton\cite{sipser96}はコンピュータの能力の限界や階層、計算量を理解するための重要な理論である。Automaton の理論に関する証明を Agda\cite{Norell:2009:DTP:1481861.1481862} で行う\cite{automaton-kono-github}。従来の教科書は一階述語論理と素朴集合論程度で書かれていて、数学的な構造や定理、証明が形式化されていることはほとんどない。Agda はプログラミング言語であると同時に定理証明系なので、Automaton の実装と、その性質の証明を同じ言語で行うことができる。Automaton の基本的な部分の証明を理解することがプログラムの信頼性を理解することにつながる。Agdaは古典的な一階述語論理と異なる証明により真理値が決まる直観主義論理であり、それを理解することは数学の証明が何かを理解することになる。特にAutomatonと非決定性Automatonの意味(language)としての同等性を簡単に示すことができる。Automatonの状態の有限性に関しても考察を行う。 | |||||||
| 書誌情報 |
第65回プログラミング・シンポジウム予稿集 巻 2024, p. 41-49, 発行日 2024-01-06 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
