coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: Mario Carneiro <di.gama AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function
Date: Fri, 19 May 2023 13:34:19 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT mailscanner.iro.umontreal.ca
Ironport-data: A9a23:TnqH6KLerGJGxRyHFE+RSJElxSXFcZb7ZxGr2PjKsXjdYENS1jQPn 2dMDDzTPvyMMWHyKdh1Yd+/p0kAuMKGx4QxGQcd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgf9s9JIGjhMsfnb9Uo+5K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LuQ0bh/vRXC08KO7Idxs9eAHhB8 aI0N2VYBvyDr7reLLOTT+Btgt8oJc/tMZlZu2tniyzcCvA6W53KR+PB7Le03h9p3ZoIR66CI ZBEL2c3BPjDS0Un1lM/DZU4mualnFH+aToetVeSo7Yt7mHXigd4uFToGIONKoPXGpgIwy50o Eri803hJDc7L+CE7nmj01Hzi9bLsxjCDdd6+LqQrKcw0QLPmgT/EiY+Xlyi5PK9l0SWQMNaM 0VS+yw0rKF0+lbDczXmdxixoXqftRcaXddKVewg70eQz63S/xyUD2xCRTcphMEaWNEedQEn6 16wmN3VAwNqjJS8SGuS8um4smbnUcQKFlMqaSgBRAoDxtDspoAvkx7CJuqP9obu1LUZ/hmrm Vi3QDgCa6Y70ZNWjf/nlbzTq3fz/caSEVddChD/AwqYAhVFiJmNTKXABbLzyPFdKprRdF6Qt XxsdyO2zLs2ZX1heeDkfQngNLSg5vKeOzTah1N1WZg78HKw/nmlYZpd6TU4L04B3ic4ld3BP hO7VeB5vcI70J6WgUlfOdrZ5yMCl/WIKDgdfqqIBueim7AoHON9wAlgZFSLw0fmm1U2nKc0N P+zKJj8USpBVfo7kmPpHI/xNIPHIAhjnQs/orinkHyaPUa2PyP9pUotaQLeML1ntMtoXi2Mr o4GXyd19/mveLenOHiIrdJ7waEiN3UgCJnr48AYd+iNJRBjEX0gDPnKiagqeoFjg6Vbl/7V8 2r1VlIQ0Ufyj3DMYUWQa2sLVV8cdcsXkJ7PBgR1ZQzA8yF6Me6SAFI3K8NfkU8PqLYykpaZj pAtJ629Pxi4Ymieo2xEMMej9uSPtn2D3GqzAsZsWxBnF7YIeuAD0oaMktLHpXBeXBmk/9Azu aOh3Q79SJ8ODVYqRsXPZf7lixv7sXEBkaggFwHFM/tCSnXKqYJKEi3WiuNoAscuLR6Y+CCW+ TzLCjglpM7MgbQPzv/3uY6+obyEKdBORnhhIzGD7JKdFzXrwW648IoRDMeKZW/8UU33yoWDZ MJU7en3Na0akGkTrYB6KadZ8owlw97Jp55b0QVWM3HZZHu7Cr5bAyen3OsekoZv17NmqQ+Nd UbXweZjOJKNI9HAPGMKAQgYMtS4yvAfnwfN4cQPIEnV4DF9+JyFWx5wOyagpTN8LrwvFq8Y2 sYk5dAr7jKghioQMtqpij5e80KOJCciV4QlrpQrP5/5uDE0y11tYY3uNQGu2cuhM+5zC0gNJ iOYoIHghL4Gn0rLTCcVJEj3hOFYgcwDhQBOwFo8PG+2o9vihMFm+D1K8D8ycBZZ8QUf7cJ3J VpQFhNUIYegwm5WofZtDkGWJhF5JRyG+0bO5UMDu0/HQmKJCGHcDm0PFtyc3UIe8mhjUCBR3 Jea+Vm4TATaXdz47gksfUhbt/a5EIR68zPCkuv6HfW+PoIbZAD9ifSEfls4qBrAAOIwinbYp OJswv1CVK3jOQMUoIw5E4O/x51KbDyhO0p5XuBHwKMFOUr+aQOC82GCBG7pc/wcOsGQ11GzD vJfA/5mVjO85X6olS8aD6tdGI1Etqcly/Rac4y6OFNclaWUqwdol5fi9iLeomsPaPc2mOYfL rLhTR6zIlayt1B1xVCU9NJlP1Cma+YqfAf/heC50NsYHqI57d1DTxsA7auWjV60bi1XpwmZr SHSVZ/wluZC87lhr6HoM6dEBji3F+/NafS1wFiNlOpKPPzyMpbolgIKq1PYERxcEpkPVv9Wy 7mckt7F83nUnbQxUmnpuYelEZdV75/vBOFSDML9ByRYrBCjQ+7p2QMIoEqjGKxKkfRcx8ipf BS5Y82ObuwoW89R6XlWSipGGTMPIv3TQoa5gg3ltNWKKBwW8TKfHeOd7XWzMF1qLH4ZCaPxG irfmqiI5OkBiK9uGRVdJfVtI6EgEW/ZQaF8KuHA72iJPFKJ3GGHlKDpzyc7yDfxDXKBLsb2z LTFSjX6dzWwoKv4985YgaMjoiwoCGtBvsdocnI/49JWjxWIPFwCJ8kZMrQEDcharHWjntWwL jTAd3ArBijBTCxJO0e0qsjqWgCEQPcCIJHlLzgu5FmZcDqyGJjGOrZ66yN8+D1jT1MPFg18x Q02oRUc/yRdw62Fgc4W7/2/muxuwPXX3DQJ40e7jsn1BQoEDLwOkndodOaIueorDOmV/Hgn5 0BsLYyHfK1/YU/rFoB9fnlTBAsUtTepxDxAgeKn3oPEo4vCpAFf4KSXBgwwu4HvqOwLPrlIW HbwQXeX7mmSnHca0UfsVxTFnocsYc+28gOGwGMPiOHcc2xcKojqAi/aoRcycQ==
Ironport-hdrordr: A9a23:CEXSzqgu/swKn3MTG6xrZE2r/nBQXv4ji2hC6mlwRA09TyVXra GTdZUgpGbJYVMqNU3I9urwXJVoLUmyyXcx2/hzAV7AZniBhILLFvAB0WKK+VSJcEeTygce79 YET0EUMr3N5DZB4/oSrDPIdOoI8Z28yYiNwcf44FEFd3ATV4hQqz1BIiLeN2FIaCwuP+tDKK ah
Ironport-phdr: A9a23:Ojp9pBaB9nBlUWWLB0MMwwH/LTHO2oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gKPBtuGoKsd0aL/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglWhDexe71/I RS2oAneq8UanJVuIbstxxXUpXdFZ+tZyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7U LJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5 LplRRP0lCsKMSMy/WfKgcJyka1bugqsqRxhzYPKfY+aNvlwfq3Tc9wUSmVOQt1cVzBdDo6mc 4cDE/AMMfpeooLgp1UOtxy+BQy0Ce3y1j9HmHH20rc80+88Fg/G2wogH9QPsHvKttX+KaAfU eWyzKnOyzXDbu1Z2S3m5YjJaBAhpuuAXa91ccrWz0kvCxnFgUuKpozhJT+ayv4CvnGd4uF9W u2hl3QppBttojiz2MgskI/Ji5oLxl3A6Sh3zpo5KNm4RUB0Y9OpFJpduj2EOoZ1QM4vQ39lt ig7x7MJuZC2ficExZcjyhPbdfCKbYuF7x3/WeieJzpzmXFreKqnihqv/0Ws1PfwWteo3FtFt CZJjNnBumoN2hDP8sSKRftw8l2u1DuAzQzf9P9ILEQumabFK5Mt3Lg9nYcJv0vZBC/5gkD2g beWdko6/uio7PzqYrD8qZ+dM490kR3xPb4omsy5H+s4KBICX2mB+eS7zrHj4Ej5QLJMjv0qi KnWrorVJcABqqGlGQBZyocj6xChADe6yNkUgHcKIExfdB6Zk4TkNEvCLO74APulg1mgjC9nx /XcMb3gBpXNIGLDkLDkfbtl7k5czwwzzdZe551KELEMO/PzWlX2tNDCEx85Ngu0w+D7CNVny IwRQ2aPDrWFP6zIqVOI4PkgLPGWZIAJoDb9N+Ql5/n2gHMkgVMdZ7Wm3YMLaHCkGfRrO1mWY X31gtsYDWgKuhc+Q/fxhV2ZUT9TYm6yULgm6jE6DoKmF4bDSZq3jLyPxifoVqFRM0VPEFGLW VzhbYOJWu0LIHaeI4lumzkNfbekQo4lkxqpsVmp5aBgK7/v5iAWvJSr8d9z4ezej1lm8DtyC cWQyUmMVWYyg2YPQSMs0al750d0nATQmZNkiuBVQIQAr8hCVR03YMa0J41SDtnzXliEZdKVU BO8Rd7gBzgtT9U3yttIYkBnGtzkgAqQlzGyDeozkLqGTIcx7rqax2L4csN6zXDH2bMJjkMhB NZKMmu6nKN2807YDt2BiF2Xwp6jbr9UxyvR7CGGxGuKsltfVVt1VqPDXH0FTkrMqpLk40TEU 6WjALBhOQISgdWaJP5sbdvkxU5DWO+lONnaZDepnHysAB+T2r6WRI/jemEG1yzbDkUe1QEJ+ jCbMA84Gj2sqmaYBzUG+UvHRUTq/KE+rXq6ShVx1ASWdwh70LHz/BcJhPuaQvdV37QeuS5np S8mVFC6l8nbDdaNvW8DNO1VfM897VFb1GnYqx01P5quKLpnj0IfdAI/tl3n1hF+AIFN2cYwq 3ZiwA13IKOemFRPElHQlZX3PLvWJ3Pa/QqoLbPT3VfCytuf/uEE4bVwqlnuuh2oClt3629ug Lw3mzOX4pTHChZXUIqkCx1tsUIi+/eAP29gv9CxtzUkK6S/vz7c1sh8AeIkzkzlZNJDKOaeE wS0FcQGBs+oIehsml6zbxtCMvoBkcx8d86gafaC37ameeh6mzfzx2FA5oZ831ik9jB7DPPN2 JAZ2fyR2k2MXn2v6TXp+tCygo1CaTwISyC6zi7iBYNLTqxoesAWDGCoP9e6z9E4jJenCBs6v BazQlgB3sGuYx+baVfwiBZR2UogqnuigSKkzjZwnlnFt4Kn1TfVi6TnfRsDYCtQQXV6yE3rK s6yhswbW06ha04okgGk7AD03foTqKN6JmjVCUBGGkq+Z2RlVK2xu6CqYtRIro4ttiNLSum1Z RaRQ/bxrgAb3CXqA2ZFjGlgLXfw4sm/xUE81TrVJW0WzjKRYcxqwBbD+NHQDeVc2DYLXmgwi DXaAES9I8j8+NyVk5nZteXtH2mlV5BVbWzq1dbZ73H9vzU2R0fi2a3rybiFWUAg3CT21sdnT 3DNpRf4OMzw0riidPhgdQ9uDUP97MxzHsd/lJExjdcewyt/5N3d8HwZnGP0Kdge17j5aS9HQ DkNxd/Y+iDkwkolM3eOwZ7jW3yZhMBoLYrfACteymcm4sZGBb3BprlDmy10r0CQrBjWJ+V4m TEB0/Yn7DgRiqta3WhlhjXYCbcUE05COCXqnBnd9NGyopJcY2O3eKSx3k5zzpixSauPqQZGV DPla48vSGVuu95nPguGgxiRosn0PcPdZtUJuliIngfc2qJLfYkpmKNCjHhiNHj2oGcoje8hi lpz2Ja8oJKKImEr96vcYFYQP2/wbsIXomirjLxZ2NuT2IazBJhoHnMAVdPhH/ehETZUtO7gc RuLFzsgsHqSHfzUFGr9oA9v/XfGEpSwPHiRInQDi9R4Q1+AIUtZnBoZVTF8lZdxFwahwNHtf RVk4zcX+kT1ox8KwesgIRD7Vi23SB6ATDAyRdDfKRNX6lsH/ELJKYmE6ek1GShE/5qnpQjLK 2qBZg0OA3tbEkqDT0vuOLWj/7yiu6CRG/a+Iv3SYL6Ptf0WVvGGwoiq25dn+DDEP9uGP31rB fk2kkRZWnUxF8PckjQJAysZ8kCFJ9acvwu58zZro9qX9f3qXBnk7I2JBqEUMM9ovQ2zhqGfL eOZgGByIHcQ158Bw2PJ1KlK3FMWjHILFXHlGrABuCjRCaPIz/YMVVhBM381bpYOsvpvu2sFc dTWgd70yLNi2/s8ClMfEEfkhtnsf8sBZWe0KFLAAk+PcrWAPzzChc/tMsbeAfVdivtZsxqot HOVCUjma36GkD/vVh21GeBWi2eGORtYpJuwexIrAmGpH7eEIlWrdcR6izE72+h+nnTRKWsVK iRxaWtIp7yU9ihRhPNyASpA9H0jMOyDnTqD4uDcbJ0f+6gOYGw8h6dR53I0zKFQ5SdPSalum SfcmdVppkmvjuiFzjcPuPVmqyxMwp+OukN+I6jQ8t9LUCSdlPrsxWCZChARrNJjDND1/aFKz Z7SkaX1NC1P+taS9sJOX6A8zeqGKn1nLB/uHiLOAQIBCzWiZzm3ug==
Ironport-sdr: 6467b321_BhcOQo7AJA9TF0N376qOm8J6aYboe2qpNy9Q1NCKrCWCr/k BnZ+S9II3M89n7RVynhaDUnHVqJbj8ZzzSLRMcQ==

> This doesn't sound quite correct. While Kleene's T tells you that for any
> terminating computation there is *some* bound for the fuel you need to
> compute the value, the bound itself might be quite large, and so you are

Side question: is it the case that such a (conservative) bound is always
computable, even for those functions whose termination proof relies on
classical axioms?

Stefan

Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, (continued)
- Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Yannick Forster, 05/18/2023
  - Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Mario Carneiro, 05/18/2023
    - Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Yannick Forster, 05/18/2023
      - Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, mukesh tiwari, 05/19/2023
        
        Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Xavier Leroy, 05/19/2023
        
        Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, mukesh tiwari, 05/19/2023
        
        Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Xavier Leroy, 05/20/2023
        Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Gaëtan Gilbert, 05/20/2023
        
        Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Vedran Čačić, 05/22/2023
        
        Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, mukesh tiwari, 05/22/2023
    - Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Stefan Monnier, 05/19/2023
      - Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Mario Carneiro, 05/19/2023
        
        Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Hugo Herbelin, 05/22/2023
- Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, Vedran Čačić, 05/18/2023
  - Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, mukesh tiwari, 05/24/2023