• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2022 年度 実績報告書

連続系における高階函数の保証つき厳密計算

研究課題

研究課題/領域番号 22F22071
配分区分補助金
研究機関京都大学

研究代表者

河村 彰星  京都大学, 数理解析研究所, 准教授 (20600117)

研究分担者 PARK SEWON  京都大学, 数理解析研究所, 外国人特別研究員
研究期間 (年度) 2022-04-22 – 2024-03-31
キーワードexact real computation / program verification / higher-order Hoare logic / constructive type theory / formalized mathematics
研究実績の概要

An imperative language for exact real number computation with pure higher-order function construction is proposed. The design is inspired by the standard functions in C++. The language is further equipped with primitive operators for countable nondeterministic choices and nondeterministic limits to make the language’s function construction useful. The language’s denotational semantics is formalized based on computable analysis and domain theory using an unbounded powerdomain for countable nondeterminism. Sound Hoare-style proof rules for the two additional primitive operations are devised. As an example, an imperative program nondeterministically computing a root of a continuous real function, a constructive variant of the Intermediate Value Theorem, is given and proved correct.

Coq-AERN is an axiomatic formalization of exact real number computation in a constructive type theory and Coq. The formalization is extended with function spaces, open subsets, closed subsets, compact subsets, and overt subsets. Similarly to the programming language counterpart, this formalization is extended with countable choices. Examples of drawing various subsets, including some fractals, in Euclidean spaces are given.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

The four steps were planned for FY2022: i) syntax for higher-order types, objects, and operations, ii) natural operational semantics, iii) domain-theoretic denotational semantics, and iv) the soundness of the semantics. Except for the operational semantics, the other steps are achieved as they were planned. A part of the achievement is submitted to an international conference and a part of the result is accepted for publication in Journal of Logic and Computation (Oxford Univ Press). Instead, some parts, including Hoare-style proof rules of some fundamental operations and the logical language part, of the next year’s plan are studied. The operational semantics part will be dealt in FY2023 when the implementation of the language is considered.

今後の研究の推進方策

There is no major deviation from the original plan FY2023. Based on the proof rules for countable choices and nondeterministic limits, we provide a complete set of proof rules to accommodate further necessary primitive operations that are to be specified further in FY2023 during seeking for example data types and operations. It may include extending the language further to have higher-order functions that cause side-effects, reference variables, and multi-threads that are communicating. Formal denotational semantics for the extensions, and their proof rules will be given. The soundness and (relative) completeness of the set of proof rules will be proven. The operational semantics of the language will be studied when we implement the language. It includes studying the possibility of including concurrent computing in realizing nondeterminism. We include several nontrivial examples and implementations for higher-order computations.

  • 研究成果

    (6件)

すべて 2022 その他

すべて 国際共同研究 (1件) 学会発表 (5件) (うち国際学会 4件)

  • [国際共同研究] Univerza v Ljubljani(スロベニア)

    • 国名
      スロベニア
    • 外国機関名
      Univerza v Ljubljani
  • [学会発表] A type-theoretical interpretation of intuitionistic fixed point logic2022

    • 著者名/発表者名
      Ulrich Berger, Sewon Park, Holger Thies and Hideki Tsuiki
    • 学会等名
      2022 Global KMS International Conference
  • [学会発表] Some steps toward program extraction in a type-theoretical interpretation of IFP2022

    • 著者名/発表者名
      Ulrich Berger, Sewon Park, Holger Thies and Hideki Tsuiki
    • 学会等名
      Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2022)
    • 国際学会
  • [学会発表] Certified exact real computation on hyperspaces2022

    • 著者名/発表者名
      Michal Konecny, Sewon Park and Holger Thies
    • 学会等名
      ontinuity, Computability, Constructivity - From Logic to Algorithm (CCC 2022)
    • 国際学会
  • [学会発表] Nondeterministic limits and certified exact real computation2022

    • 著者名/発表者名
      Michal Konecny, Sewon Park and Holger Thies
    • 学会等名
      Nineteenth International Conference on Computability and Complexity in Analysis (CCA2022)
    • 国際学会
  • [学会発表] From Coq Proofs to Efficient Certified Exact Real Computation2022

    • 著者名/発表者名
      Michal Konecny, Sewon Park and Holger Thies
    • 学会等名
      Proof and Computation 2022
    • 国際学会

URL: 

公開日: 2023-12-25  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi