• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Computational complexity and practice of verified and efficient algorithms for dynamical systems

Research Project

Project/Area Number 20K19744
Research Category

Grant-in-Aid for Early-Career Scientists

Allocation TypeMulti-year Fund
Review Section Basic Section 60010:Theory of informatics-related
Research InstitutionKyoto University (2021)
Kyushu University (2020)

Principal Investigator

THIES HOLGER  京都大学, 人間・環境学研究科, 特定講師 (50839107)

Project Period (FY) 2020-04-01 – 2024-03-31
Project Status Granted (Fiscal Year 2021)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
KeywordsComputable Analysis / Exact Real Computation / Formal Proofs / Proof Assistants / 計算可能解析学 / 計算量 / 計算機援用証明 / 実数計算 / Computable analysis / Differential equations / Verification / Formal proofs / Complexity Theory
Outline of Research at the Start

The research project aims to get insights into the computational complexity of problems in the physical world and to provide efficient and formally verified algorithms for computations that involve real numbers. Such algorithms lead to better, more reliable and reusable software.

Outline of Annual Research Achievements

The project can be broadly divided into two parts, the first dealing with complexity of differential equations and exact real computation (ERC) algorithms, the second dealing with formalizing ERC in the Coq proof assistant.
Regarding the first part, novel algorithms for computing solutions of certain partial differential equations (PDEs) were found and shown to behave well in terms of complexity. In particular, the focus was on linear PDEs with analytic matrix coefficients and the Heat and the Schroedinger equation with given analytic initial data. The algorithms were implemented in the ERC framework iRRAM and tested on several practical examples.
Regarding the second part, together with international collaborators a new framework for formal verification of ERC based on a type-theoretical setting was derived. The type-theoretical setting is chosen to be simple and allows a realizability interpretation to validate certain axioms in the theory. Building on the framework a new formalization of ERC in the Coq proof assistant was built. The formalization is conceptually similar to modern implementations of ERC and it allows to extract efficient Haskell programs from proofs. The extracted programs use the AERN framework, a popular Haskell framework for exact real computation, for basic operations on real numbers.
Lastly, comparisons to other formal proof systems, in particular the system IFP have been made. IFP is based on intutionistic fixed point logic and is mainly used for the extraction of ERC programs from proofs, and thus comparing the two approaches lead to new insights.

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

Large progress was made for both parts of the project.
Regarding PDEs, several new algorithms based on power series have been devised and implemented in the iRRAM C++ framework. The results were published in the proceedings of a well-known international conference (CASC 2021) and the PI presented the results at invited talks at CCA2021 and an autumn school on proof and computation.
Progress was also made on the formalization of ERC in the Coq proof assistant. The new type-theorical framework devised during this AY allowed to quickly prove several results in the proof assistant and progress was faster than initially planned. Further, the extraction directly to an ERC framework is a new idea that had not been considered before and lead to much more efficient extracted code.
First results have already been published in the proceedings of WoLLiC2021 and further results have been accepted for publication at Nasa Formal Methods 2022.
Some smaller results on the comparison to the formal system IFP have also been presented at workshops.
Still, the ongoing Covid-19 pandemic made international collaboration difficult. Although online meetings were helpful, they could not completely replace physical meetings. As the project is done in close collaboration with international researchers and progress could have been faster without the ongoing restrictions.

Strategy for Future Research Activity

First, it is planned to summarize the currently obtained results on the formalization of ERC in a larger journal publication.
Afrer that the framework will be extended to other mathematical operations.
In particulat, a representation for spaces of functions will be considered that makes it possible to implement not only functions but also operators and functionals on real numbers. Other extensions that will be considered are matrices of real and complex numbers and operations like computing eigenvalues and Matrix diagonalization. Furtehr, more theoretical work on relating results on classical real numbers in Coq to our implementations of real numbers will be conducted.
Regarding algorithms for differential equations, it is planned to collaborate more closely with numerical scientists and devise solution methods of other forms of PDEs and their extension to ERC. Possible applications include fluid dynamics and other areas of physics and such applications will also be considered.
Finally, it is planned to unify the two parts of the project. In particular, the extension to spaces of functions allows to consider operations like integration and solution operators for ordinary and partial differential equations. The ERC algorithms which have been found can then be formalized and be proven correct in Coq. To this end, some classical mathematical results about differential equations also need to be proven in Coq.

Report

(2 results)
  • 2021 Research-status Report
  • 2020 Research-status Report

Research Products

(16 results)

All 2022 2021 2020 Other

All Journal Article (5 results) (of which Int'l Joint Research: 5 results,  Peer Reviewed: 5 results,  Open Access: 2 results) Presentation (10 results) (of which Int'l Joint Research: 9 results,  Invited: 3 results) Remarks (1 results)

  • [Journal Article] Computable analysis and notions of continuity in Coq2021

    • Author(s)
      Florian Steinberg, Laurent Thery, Holger Thies
    • Journal Title

      Logical Methods in Computer Science

      Volume: 17:2

    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Axiomatic Reals and Certified Efficient Exact Real Computation2021

    • Author(s)
      Konecny Michal、Park Sewon、Thies Holger
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 13038 Pages: 252-268

    • DOI

      10.1007/978-3-030-88853-4_16

    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Exact Real Computation of Solution Operators for Linear Analytic Systems of Partial Differential Equations2021

    • Author(s)
      Selivanova Svetlana、Steinberg Florian、Thies Holger、Ziegler Martin
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 12865 Pages: 370-390

    • DOI

      10.1007/978-3-030-85165-1_21

    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Continuous and Monotone Machines2020

    • Author(s)
      Michal Konecny, Florian Steinberg, Holger Thies
    • Journal Title

      Leibniz International Proceedings in Informatics (LIPIcs)

      Volume: 170

    • Related Report
      2020 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Computable Analysis for Verified Exact Real Computation2020

    • Author(s)
      Michal Konecny, Florian Steinberg, Holger Thies
    • Journal Title

      Leibniz International Proceedings in Informatics (LIPIcs)

      Volume: 182

    • Related Report
      2020 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Presentation] An application of constructive dependent type theory to certified computation over the reals2022

    • Author(s)
      Holger Thies
    • Organizer
      The second Korea Logic Day
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] Extracting exact real computation programs from proofs in type theory2022

    • Author(s)
      Holger Thies
    • Organizer
      The second Japan-Russia workshop on effective descriptive set theory, computable analysis and automata
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] Uniform Complexity of Solving Partial Differential Equations and Exact Real Computation2021

    • Author(s)
      Holger Thies
    • Organizer
      18th International Conference on Computability and Complexity in Analysis
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] IFP style proofs in the Coq proof assistant2021

    • Author(s)
      Holger Thies
    • Organizer
      Continuity, Computability, Constructivity - From Logic to Algorithm
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] Complexity Theory in Analysis with Applications to Differential Equations2021

    • Author(s)
      Holger Thies
    • Organizer
      Autumn school Proof and Computatio
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] Axiomatic Reals and Certified Efficient Exact Real Computatio2021

    • Author(s)
      Holger Thies
    • Organizer
      27th Workshop on Logic, Language, Information and Computation
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] Toward an interpretation of Intutionistic Fixed Point Logic in Coq2021

    • Author(s)
      Holger Thies
    • Organizer
      The 17th Theorem Proving and Provers meeting
    • Related Report
      2021 Research-status Report
  • [Presentation] Computable analysis and exact real computation in Coq2020

    • Author(s)
      Holger Thies
    • Organizer
      Fourth Workshop on Mathematical Logic and Applications
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] Continuous and Monotone Machines2020

    • Author(s)
      Holger Thies
    • Organizer
      45th International Symposium on Mathematical Foundations of Computer Science
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] Computable Analysis for Verified Exact Real Computation2020

    • Author(s)
      Holger Thies
    • Organizer
      40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Remarks] Personal Homepage

    • URL

      http://www.holgerthies.com

    • Related Report
      2021 Research-status Report 2020 Research-status Report

URL: 

Published: 2020-04-28   Modified: 2022-12-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi