ダウンロード数: 42
このアイテムのファイル:
ファイル | 記述 | サイズ | フォーマット | |
---|---|---|---|---|
LIPIcs.MFCS.2023.59.pdf | 1.11 MB | Adobe PDF | 見る/開く |
完全メタデータレコード
DCフィールド | 値 | 言語 |
---|---|---|
dc.contributor.author | Konečný, Michal | en |
dc.contributor.author | Park, Sewon | en |
dc.contributor.author | Thies, Holger | en |
dc.date.accessioned | 2024-02-28T02:16:17Z | - |
dc.date.available | 2024-02-28T02:16:17Z | - |
dc.date.issued | 2023-08-21 | - |
dc.identifier.uri | http://hdl.handle.net/2433/287104 | - |
dc.description | 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) | en |
dc.description.abstract | We propose a framework for certified computation on hyperspaces by formalizing various higher-order data types and operations in a constructive dependent type theory. Our approach builds on our previous work on axiomatization of exact real computation where we formalize nondeterministic first-order partial computations over real and complex numbers. Based on the axiomatization, we first define open, closed, compact and overt subsets in an abstract topological way that allows short and elegant proofs with computational content coinciding with standard definitions in computable analysis. From these proofs we extract programs for testing inclusion, overlapping of sets, et cetera. To improve extracted programs, our framework specializes the Euclidean space ℝ^m making use of metric properties. To define interesting operations over hyperspaces of Euclidean space, we introduce a nondeterministic version of a continuity principle valid under the standard type-2 realizability interpretation. Instead of choosing one of the usual formulations, we define it in a way similar to an interval extension operator, which often is already available in exact real computation software. We prove that the operations on subsets preserve the encoding, and thereby define a small calculus to built new subsets from given ones, including limits of converging sequences with regards to the Hausdorff metric. From the proofs, we extract programs that generate drawings of subsets of ℝ^m with any given precision efficiently. As an application we provide a function that constructs fractals, such as the Sierpinski triangle, from iterated function systems using the limit operation, resulting in certified programs that errorlessly draw such fractals up to any desired resolution. | en |
dc.language.iso | eng | - |
dc.publisher | Schloss Dagstuhl Leibniz-Zentrum für Informatik | de |
dc.rights | © Michal Konečný, Sewon Park, and Holger Thies | en |
dc.rights | Creative Commons Attribution 4.0 International license | en |
dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | - |
dc.subject | Computable analysis | en |
dc.subject | type theory | en |
dc.subject | program extraction | en |
dc.title | Formalizing Hyperspaces for Extracting Efficient Exact Real Computation | en |
dc.type | conference paper | - |
dc.type.niitype | Conference Paper | - |
dc.identifier.jtitle | Leibniz International Proceedings in Informatics (LIPIcs) | en |
dc.identifier.volume | 272 | - |
dc.identifier.spage | 59:1 | - |
dc.identifier.epage | 59:16 | - |
dc.relation.doi | 10.4230/LIPIcs.MFCS.2023.59 | - |
dc.textversion | publisher | - |
dcterms.accessRights | open access | - |
datacite.awardNumber | 22F22071 | - |
datacite.awardNumber | 20K19744 | - |
datacite.awardNumber | 23H03346 | - |
datacite.awardNumber.uri | https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22KF0198/ | - |
datacite.awardNumber.uri | https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20K19744/ | - |
datacite.awardNumber.uri | https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23H03346/ | - |
dc.identifier.eissn | 1868-8969 | - |
jpcoar.funderName | 日本学術振興会 | ja |
jpcoar.funderName | 日本学術振興会 | ja |
jpcoar.funderName | 日本学術振興会 | ja |
jpcoar.awardTitle | 連続系における高階函数の保証つき厳密計算 | ja |
jpcoar.awardTitle | Computational complexity and practice of verified and efficient algorithms for dynamical systems | en |
jpcoar.awardTitle | 連続な空間上の計算とその複雑さの研究 | ja |
出現コレクション: | 学術雑誌掲載論文等 |
![](/dspace/image/articlelinker.gif)
このアイテムは次のライセンスが設定されています: クリエイティブ・コモンズ・ライセンス