Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Quite complex functions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Quite complex functions


Chronological Thread 
  • From: Castéran Pierre <pierre.casteran AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Quite complex functions
  • Date: Tue, 29 Dec 2020 10:33:20 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.casteran AT gmail.com; spf=Pass smtp.mailfrom=pierre.casteran AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f54.google.com
  • Ironport-phdr: 9a23:9b+XIxautofWVMSs7KZzlw3/LSx+4OfEezUN459isYplN5qZrsy/bnLW6fgltlLVR4KTs6sC17OJ9fq6ACdYuN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6txvdutcLjYdtNqo91wbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrRyhuxNxzIHbbpyWOvRwYK3TesgXRXZYXsZUSyBBAp+wYokJAuEcPehYtY79p14WoBagHwasH//vzSVShnDs2601y/4vEQDY0ww6BdIBrmnfodLtNKcTT++11rPIwivZY/xKwzj985TIfQ47of6WW7J9asXRyUw1GAPEilWcs5DqPzSQ1ukUtWWQ8uVvW/61hWE9twFxviagxt0qioTRm44YykzJ+Tt3zos1OdG2SFB2bMCgHZZfqi2UOZZ7T80tTm11uSs21rMItJy/cSUO1Zkq2hzSZvyIfYWJ4x/uSuCcKip7inJ9YL+zmQq+/Ey6xuD/VsS4yktGojRGn9XWtn0A2ATf5tadRfdh40us3CqA2BvO5uxAJE05l7HUJp4kz7M+iJUfrVjPEyrtl0jygqKbdUAp+ua05Oj6frrro4KTOoB6igz+N6kjmNKzDfolPgUIQmOV4/6z1Kf58k38WLhKjuM5kq3esJ3CIMQUvK+5AwtM3oct7hazEi6q0NoYkHQINl5FdxWHj4/mO1HKPv/0F+uwg1OpkDtzxvDGOKPuAonVI3TdjLvseaxx5k1cxQYp0NxT+ZFZBqsBLf/8QkPxscbXDh49Mwy62ebnD9B925sGWWKOHKCZKrnSvkGS6u0zOeaMf5MVtyjnK/c/4f7jlnA5mVoHcqmo2Zsbcmy3HvNjI0mBe3rjns8BEXsWvgo5VOHllFqCUSdKa3muW6I8+yo0BZm9DYbDQ4CtmKaO0D26Hp1QfGBGC0qDHW3md4WeCL8wb3eZJdYkmTgZX5CgTZUg3FegrlzU0b1ie8Hd4TGZr5vl4+B06vfJmFlm7T15Fd6QlWqEVH15hGoObzAz1aF750d6zwHQguBDn/VEGIkLtLtyWQAgOMuElrEoO5XJQgvEO+yxZhOmT9GhW2xjS9swx5oRZh84FYj+yB/E2CWuDvkekLnZXMVooJKZ5GD4IoNG81iDzLMo1gB0Tc5GNGngjal6pVCKVtz51n6BnqPvTpwymSvE9WON122L5RgKXwt5UKGDVncaNBLb

Hi,

I’m interested in formal proofs about rapidly growing functions, like :
« The Ackermann function is not primitive recursive » (folklore)
« The Hardy function H_(omega^alpha) has essentially the same order of
growth than the Wainer function F_alpha » (Ketonen and Solovay).

Do you know an already existing library about this topics ?

Thank you in advance,

Pierre





  • [Coq-Club] Quite complex functions, Castéran Pierre, 12/29/2020

Archive powered by MHonArc 2.6.19+.

Top of Page