...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>LIPIcs : Leibniz International Proceedings in Informatics >Formalizing Computability Theory via Partial Recursive Functions
【24h】

Formalizing Computability Theory via Partial Recursive Functions

机译：通过部分递归函数形式化可计算性理论

获取原文
   

获取外文期刊封面封底 >>

       
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We present an extension to the mathlib library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and we use a constructive encoding of partial functions such that they are executable when the programs in question provably halt. Main theorems include the construction of a universal partial recursive function and a proof of the undecidability of the halting problem. Type class inference provides a transparent way to supply G?del numberings where needed and encapsulate the encoding details.
机译：我们提出了对精益定理证明者的mathlib库的扩展，形式化了可计算性理论的基础。我们使用原始递归函数和部分递归函数作为研究的主要对象，并且使用部分函数的构造性编码，以使当所讨论的程序停止运行时，它们可以执行。主要定理包括通用局部递归函数的构造以及中止问题的不确定性证明。类型类推断提供了一种透明的方式，可以在需要时提供Gdel编号并封装编码细节。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号