On Recursive Functions and Well—Founded Relations in the Calculus of Constructions

机译：关于构造演算中的递归函数和有根据的关系

获取原文

获取原文并翻译 | 示例

页面导航

摘要
著录项
相似文献
相关主题

摘要

This paper presents a reflection about function construction through well-founded recursion in the type theory known as Calculus of Inductive Constructions. It shows the expressive power of this calculus when dealing with concepts as accesibility and noetherianity among others. The properties of the General Recursion Scheme ([2]) and its relation with Structural Recursion in inductive types are analyzed. As a consequence, a methodology arises which is illustrated with some examples. We use the INRIA's compiler of the Calculus of Inductive Constructions: Coq.

机译：本文通过被称为归纳构造演算的类型理论中的有据可归的递归，对功能构造进行了反思。它显示了这种演算在处理诸如可访问性和无网络性等概念时的表达能力。分析了一般递归方案（[2]）的性质及其与归纳类型中结构递归的关系。结果，出现了用一些示例说明的方法。我们使用INRIA的归纳构造演算：Coq的编译器。

著录项

来源
《International Conference on Computer Aided Systems Theory(EUROCAST 2005); 20050207-11; Las Palmas de Gran Canaria(ES)》|2005年|P.69-80|共12页
会议地点 Las Palmas de Gran Canaria(ES)
作者
J.L. Freire; E. Freire; A. Blanco;
展开▼
作者单位

University of A Coruna, Department of Computer Science, LFCIA, Campus de Elvina, 15071 Coruna, Spain;

展开▼
会议组织
原文格式 PDF
正文语种 eng
中图分类机器辅助技术;
关键词

相似文献

外文文献
中文文献
专利

1. Relations Among Certain Generalized Hyper-Geometric Functions Suggested by N-fractional Calculus [J] . Maged Gumaan Bin-Saad Mathematics Letters . 2016,第6期

机译：N分形演算表明的某些广义超几何函数之间的关系
2. On the multi-index (3m-parametric) Mittag-Leffler functions, fractional calculus relations and series convergence [J] . Jordanka Paneva-Konovska Central European Journal of Physics . 2013,第10期

机译：关于多索引（3m参数）Mittag-Leffler函数，分数阶微积分关系和级数收敛
3. Multiple (multiindex) Mittag-Leffler functions and relations to generalized fractional calculus [J] . Virginia S. Kiryakova Journal of Computational and Applied Mathematics . 2000,第1期

机译：多个（多索引）Mittag-Leffler函数以及与广义分数演算的关系
4. On Recursive Functions and Well—Founded Relations in the Calculus of Constructions [C] . J.L. Freire, E. Freire, A. Blanco International Conference on Computer Aided Systems Theory(EUROCAST 2005) . 2005

机译：关于递归函数和建筑微积分中的良好关系
5. Calculus students' understanding of the derivative in relation to the vertex of a quadratic function. [D] . Burns, Annie. 2014

机译：微积分学生对与二次函数的顶点有关的导数的理解。
6. Applied Anatomy: The Construction of the Human Body Considered in Relation to Its Functions Diseases and Injuries [O] . 1930

机译：应用解剖学：考虑到人体的功能疾病和伤害的构造
7. Elements of the Differential and Integral Calculus, by a new Method, founded on the True System of Sir Isaac Newton, without the Use of Infinitesimals or Limits Elements of the Infinitesimal Calculus, with Numerous Examples and Applications to Analysis and Geometry On a New Method of Obtaining the Differentials of Functions with Especial Reference to the Newtonian Conception of Rates or Velocities [O] . R. TUCKER 1877

机译：差分和整数微积分的元素，通过一种在Sir Isaac Newton的真实系统上创立的新方法，而不使用无限的微积分的限制，具有许多实例和应用来分析和几何形状的新方法获得特殊参考牛顿率或速度的差异差异

On Recursive Functions and Well—Founded Relations in the Calculus of Constructions

摘要

著录项

相似文献

相关主题

期刊订阅