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: Vedran Čačić <veky AT math.hr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function
Date: Mon, 22 May 2023 11:53:10 +0200
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass (sender ip is 161.53.8.15) smtp.rcpttodomain=inria.fr smtp.mailfrom=math.hr; dmarc=pass (p=none sp=none pct=100) action=none header.from=math.hr; dkim=pass (signature was verified) header.d=math.hr; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=4An9jLHHdYybpEqdbHXV7FPhHi/pJyJg0bjcwt838VE=; b=KFo1L5si82QzEgd7Q6h5Fh4KCkzTsJpJj0uyru4PaBiaLtSuRWgAl8tPG1ch6CE90uxniqBBgW2omIkiwoaBaeAbjstiJzN4JJntSqb2DSKCWHk+y21zgTAlXRb4dcdoPri/3TC+yx9yFYAR3UmQ6qNRwnoslKWVww0gglshhAPUiA8UtAfbfEJDHPui5BkaZpjarUwJwqZ843kBDOGh+1T5bHRK4Q2Moc6HQeXjf8AqbgdfVASNDL9+H/f1lUEYv5TXaF9RX+GSWarrnduV8Xk9ErtGlR7LLbMQc0HEFe1QBofb/hG52fTm8C29iJn7IGyDe2FCufUmyB0VbPFmlg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=QoetCBJ9a7ZvvI8iYIoYYaQISdfT0QhGZ++zLjACfgebfo+iFDkLdna7UL7MNLQ4OHBDs2IVaRupBLPpygFMgroGO2/OZnSMiyvjonoU5pTWwvkiJKOSKRntzg7N0TD4uAKHQJT4yCGoB4oG1x58G4Oz/3Pe8WFAlnGU+uBa8t32f4n3jgvLh0OSM0qIsSmnCSY8pO9fwc4z0VfpelfhOAB1tlDwhvBLfebMzEiY2NratNktdtpqDOrJXKWowQ9cRzifrN6qKh83T0yhL7KHhs2J+ompNuxQXVJsWxXwg/sIuTe7KA9UYG9+Yp1muk31nzkHT/Qjw9UBhiAB3sZgww==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=veky AT math.hr; spf=Pass smtp.mailfrom=veky AT math.hr; spf=Pass smtp.helo=postmaster AT EUR05-AM6-obe.outbound.protection.outlook.com
Ironport-data: A9a23:DQOrYK2cEE5r67bUKfbD5Zl6kn2cJEfYwER7XKvMYLTBsI5bp2cAy WBNDW7XbvnYZGf9fdp2YYjl8RkPv8DdyNI1TwNu3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn9g1aYDkpOs/jY8E415qyr0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW0PN++o3BlsHB4YR3PcwDV0X+ sY/dS9YO3hvh8ruqF66YsRRvJx+aeDOYsYYsHwmyizFB/E7R5yFW7/N+dJTwDY3gIZJAOraY M0aLzFoaXwsYTUTYhFOUM14xr3u3yGmG9FbgAr9Sa4f/WXQ3SR02aTtdtrPEjCPbZwNzx7A/ jyZpAwVBDlAGtGQ+SXU00j3xdTOgTyjaJsjEpGRo6sCbFq7nTVIU0VPDzNXu8KRgUmnHtlbN kY84TsrtaF09UqxT9C7UQfQnZKflhsVWt4VGuhk5RyXkvfT5VzAXjFCSSNdYts7ssNwXSYty lKCg9LuA3poraGRTnWesLyTqFteJBT5M0c6RBcbFAEf0uPoqaciyR7zF9lZN/Oq24id9S7L/ xiGqy03hrM2hMEN1rmm8V2vv95KjsiWJuLSzlWHNl9J/j+Vd6b4Pdf3tAmzAeJocNbIEQTpU G0swZD20QwYMX2avAqpKAnnNJis/OqIKjHVhDaD9LF4r233k5JPVaZX+i1+bGduNsINfzOBX aM+kQZY5ZsWNX70YLJtO9+2DZ5zlfGmEsn5XPfJaNYIeoJ2aAKM4CBpYwiXwnzpl08v16o4P P93kPpA715KVcyLLxLvF4/xNIPHIAhjnQs/orimk3yaPUK2PiL9dFv8GALmghoFxK2Fuh7J1 N1UKtGHzR5SOMWnPHmLr99IfQpVciljbXwTlyCxXr7cSuaBMDFwY8I9PZt7IOSJYowJyb+Vo CnsBye0NnKm3yebd1/iho9fhEPHBs8k9ipiZ0TAzH6t2nM5Zp2o4rtXfokqZ7RPyQCQ5a8cc hXxQO3ZWq4nYm2fpVw1NMChxKQ8LkjDrVzVZUKNPmNgF6OMsiSSp7cIiCO0qHJRZsd23ONiy 4CdOvTzGstYHF85XZmHMZpCDTqZ5BAgpQ67ZGOQSvE7Rakm2NECx/XZ36ZrcfIfYw7O3CWb3 AuwCBIV77uF6Yws/dWDwejOo461GqEsVgBXDkvK34aQbCP6x2uExZMfceCqeTuGanj41p//b spoztb9EsY9onB0j6RGHY1G95kOv+nUm+cCzyBPPmn6UFCwO7YxfliExZZus4NO9J94uCy3e F6+yuNdHbCJKeLkD18jCw43ZcuT1fwvu2fz7NZkBG7Y9SNI7L68fkEKBCa1iQtZN6pTDIMp5 cwDqfwmwVWzpTRyO+nXkx0O0XqHK0IxdpkOt7YYMdfNsRUqwFQTWq7sIHb6z7/XYuodL3RwB CGfgZfDoLFuxkDiVX4XPlqV1Mp/gaU+gjx7/GUgFX+oxOWc3uQW2SdP+wsZVg5WlxVL89xiM 1hRanFaG/+8wCdKtuNiAUacQxpMFT+IyHzXklEprlDUf2Osd27KLVA+B9qzwVAkwzpcUAR2r LC840T5YAnuZ/D0j3cTW1Y6ivnNTu5R1wzlmeKJIfqkAL8BOBDZvp6ybzAqrz/iUJo9q2/Zq dY3/8J2Q7zxbhQUkvYBE4PAiakaEy7cLkMTX/hwoaEDRzndXBqQ2jG+DV+7Ve0QBv7N8G6+U 9dPIOAWXTuA9S++lBIpLo9SHK1Rg9gS+8skRrzwAGwN7p+zj2ZM6crL1y7cgGQLfY1fofwlI NmMSwPYQ32iu3REvkTs8uxWMXWcSvsZblTe2OuVzr04J6gbursxTXBog6qGhFTLAg5J5BnOg RjiYZXRxOlcyYhBuYvgP6FAJgesI+PIS+W631GvgutKcO/wH5/ChyENpnnjGjZmD78bdtB0t LaK6dDMzBzkupQyWDvngJWvLfRCyvize+t1CfjJCkdmsxGMYvKx3CtbyVuEccRItPh/+viYQ xCJbZrsVNwNBPZY6n5nSwlfNBc/F5XHVKDEoCOsjvWTCyoy1R7MA8On+ETIM0BaVH4sEL/vB jDkv82B4ohjk71NIxsfFtdaA5NcC33ya5sMLtHem2GRMTi1vwmkpLDnqysF1RjKLXu1SODB/ pPPQ0nFRiSY4a3n4olQjN1vg0cxEn14vOgXe3Ad8f5QjxSRLjYPDcYZAKU8JqBkqA7A/7CmW 2iVd0onMzv3Yhpcexal4NjDYBaWNtZTBvjHfA4W72GmQAboIrPZDLVYo3Iqpz88fzb41+ioJ O0P4nC6bFD73phtQv1V/fChx/tuwvTB3H8T5EThiIrIDg0DBakRnmlUdOaXufcrz+mW/KkKG YQ0eYyAaGyGcxasVO9FJTtSEhxfuy7zxTI1ayvJ2MzYp4iQ0OxHzrv4Jv331boAKs8NIdbig FvpEnCV7Tn+NmM74MMUVxAB2MeYys5n2uC/JbPjAw0I9011wnpyJNsMxELjU+l7kDOy0Drhe v2E5nEiBAKFMii9HVFQJRoho/pMb57HM90FYMMTa9MLfdzVAuU1oySX8T8=
Ironport-hdrordr: A9a23:Yv2YE6ghLHgqVJ1RHJhtvkPZnHBQX/Z13DAbv31ZSRFFG/FwyP rCoB1L73XJYWgqM03I+OrwSZVoJEmxhPtICOYqTM2ftWXdyRCVxcRZnPPfKl7bakvDH4xmpN tdmsFFYbWeYykYsSvj2mmF+pQbsaC6GciT9JfjJhxWPH5Xgs9bnnlE4zKgYz5LrUR9dNEE/V mnl6h6jgvlV3AebsH+IGIEUejFr9iOsJ79exYJC1oGxWC1/E6VAXLBYnyl9yZbdwkK7aYp8G DDnQC8zqK/s8ujwhuZ7GPX54Q+oqqW9jMWbvbstuElbhHXziq4boVoXLOP+Bovpvu01VosmN 7Q5z89IsVa8RrqDyGIiCqo/zOl/Ccl6nfkx1Pdq2Dku9bFSDUzDNcErZ5FcyHe91ErsLhHoe N2Nlqixtlq5C777WvADpnzJl1Xf3OP0DcfeDso/jJiuYh3Us4nkWVQxjIWLH46JlOP1GkWKp gdMCji3ociTbq7VQGRgoA9+q3lYp10JGbNfqHKgL3z7wRr
Ironport-phdr: A9a23:L26d9BYlPwCtendoW2CFQfH/LTEd2YqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gKPBtqCoKsZw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtIiTanb75/L gi6oQrMusQWnIBvNrs/xhzVr3RHfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQ LJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4 btnRAPuhSwaMTMy7WPZhdFqjK9Drx2hqR5wzY7abo+WKfRwYL/ScMgASmZdRMtcTTBNDp++Y oYJEuEPPfxYr474p1YWohSxGxSjBPn1xT9Om3T7w7c13PggEQ7awQctGMwOv2rXrNT1L6oSV Pq6zLXIzTnZb/NWwy7w5Y7VeR8uvf+CR6h/cdbNyUYxDQPFiE2dpZDqMj6b2OkAvHaX4u5uW O6yj2Mpqw58rzmsy8oil4XFmo0bxFDZ+Clk3Is4JN21RkBlbdK4E5Zdqi6UOYtyT84kXmpmu z46x6UJtJKnZiQG1YgryhzFZ/CZbYSE+A/vWPqMLTtgmX5oea+ziwyy/EWu0OHxVdO43EtKo ydDj9LCrGoC1wbJ5ciCUvZ9/lmu2TKI1w3L5e9LL1w6mbbbJpI43rM+kZsevV3EHiDthkr6l qiWdlg4+uez7OTnf7PmqYKGO49skAH+NbguldKjDuQkMwgOWG6b9f671L3+4U35RLJKjvo1k qXDrJ/aIsEbqra4Aw9TzIkj9w6yAji63NgCgHULMFBIdAiZg4T3IV3CPez0Aeqnj1Spijhrx vTGPrP7ApXKK3jOiKnhcqh+609c0wczyMpQ545UCr0bIPLzQFf9tNrDARAhKQy73/7nCMlh1 oMZQW+DH7eVMLnOvl+Q+uIvP+6MaZcJtzb6Mvgp/uLhjXskmVAGZqSpxpsWaHWgHvt8OUmZY Hzsgs0AEWgQpAY+Qvbq2xW+VmtYYG/3VKYh7Bk6DpinBMHNXNODmruEiRm2EodfYChtA1uNG j+8aYiHSt8JYT6SZM97xG9XHYO9QpMsgEn9/DTxzKBqe7K8EkwwsJvi0IIw/OjPjVQo8jcyC c2B0maLRmUyn2USRjZw0ros6VdlxAKl1q51y+ddCcQV/+lABxk3No/0yuVmC5byQFGJZc+HH W6vWc7uGjQtVpQ0yt4KbVx6HoC8gxPS9y+jH79Tl6bYTIcs/Pfk1mPqb914126A1KQliAw+R dBTMGS9mqNl3yXuPdaU1my8yeOtf6la2zPR/mCey2bIpFtfTAN7TaTCWzYYe1fSqtP6oEjFS tdCEJwBNQ1MgY6HI6pOMJjyiEleAe3kM5LYan6wnGG5AVCJwKmNZczkYTdV2iKVE0UCnw0Jm BTOfQEjGiespX7fBz1yBBruZU3r6+x3tHK8SAc90QiLa0Rr07f99AQSgLSQTPYa37RMvylEy X08Alu+zvrTAsaA4Qp7Pe1dbd47/FZbxDfBrQUudpekLq1kmhsfa1Er5wW3j0oxUN8GyJBz/ xZIhEJoJKmV0U1MbWad1JH0YPjML3XquQqoYOjQ003f19Cf/uEO7u45ohPtplLMdAJq/nN53 t1Sy3bZ6I/NCV9YT5/yQ24y/gR64bHAKHp198bP2HtgPLPh+CHP2MMBAeI5ylCgZZ0MVcHMX B+3GMocCc+0LeUskFX8dRMIMtdZ86ssNt+nff+LsEKyFN5phynuzWFO4YQnl1mJ6zI5UOnDm ZAM3/Cf2AKDETb6llao9M7ty8hIYjQbH2z3ziaBZsYZeKBxbK4OAHuuZc2tjtlznJ/iXXdE+ UXrWwtAgZf2P0DIKQWlhEVZzgwPrGaimDekwjA8iDwvoqeFnUmsi6zjeBcBJm9XVTxnhFboL 5KzioNSV0ypYg410Rq9sBqigfED++IldS+KGR4bGkq+Z3tvWaaxqLeYNstG6Zdy9D5STPz5e 1eRDLj0vxod1SrnWWpY3jEyMT+w6fCb11R3jnyQKHFroT/XY8Z1kF3B6d/NbftYwjpARDMy2 nHHQ0OxOdWk54DeiZrAo8i7Xn6hEJ1JO3qOr8vIpG6w4mtkBge6lva4l4j8EAQ05iT80sFjS STCqBuvKpmuzamxNvhrO1V5HFKpodQvAZlwy8Fj4fNYkWhfnJie+mAL1Hv+IckOk7yrd2IDH HYK24KHvFCjiRcldjTRgNukHnSFnpk9P5/jOjxQgmRlqJkUbcXcpL1cwXko+Bzh9VqXOb4l2 W5Bgfo2tCxD271P5FVrlmPFRelNVUhAY362nkzRvYnn9fdZOD73I+r3iBob/5jpDanc8FtVA C+rI857TyEstp4tYhWQgTXy8t+2ItCINIBK70TGnUuY1LoFcMppxKhN2HICWyq1vGV7mbQy1 UU8hMjj7obbcz4/9/rhWkwKcWCsL8ILpGO3hP4HzJ/PhtKhQs06SDtTBMO6H7X1SnpXvPDjf W5iCRUEo2yAUfraFA6bsgJ9qm7XVoqsPDeRLWUYytNrQF+cIlZeiUYaRmdykpk8HwGsjMvvF SUxrigW/UL9owBQx/hAGiTFCjqajSL2LzA+Rd6YMQZc6RxE6wHNK8uC4+lvHiZeuJq8sAiKL W/dbANNaANBEkCJHFHsOLCy6MKIr7DeX7LhaaGUJ+zW8KRXTL+QyIiq05d68jrELciJMnR4T rU61kdFQXFlCpHZljEIGEl132rGa8+Wogv5+zUi8pj5qay0Hli1o9LXUug3U50n4R29jKadO vTFgS94LWwdzZYQ3TrSz7NZ2lcOiiZofj3rELIatCeLQriD/80fRxMddS53M9NFqqwm2QwYc 9DWicLd07dkjrg1ER0WMD6p0tHsfsEML2ynYRnfA12XMb2dOTDR6+zKW/vhDJR10qBTvRD2v iuHGUj+ODjFjyPuSx2kLeBLimecIQBav4a+NB1qDCKwKbCuIg3+O9hxgzosxLQyjX6fLm8QP w93dEZVp6GR5ydV0b1vXnZM5X1/IayYij6UuqPGf40Ov6IhUUEW36pKpW43wLxP4GRYSexpz WHM+8V2rQjuk/HTmGY/FksU7G4N3MXS4A1jIfmLqsEGAC6bukpLtSLJVXFo75NkEoG95voWk 4CX0vq1cHAbr5rV5ZdOXpCIbp7YdiJnaV2wR3bVFFVXFzfzbDOG3hUPnq3Kri/H6cRqz/qk0 JsWFO0BXQRsRKpDUxZrQIRZcsUwAmJskKbF3pQBvSPs9UCIFssG5suVBqrKWae9b2vB6NsML xoQn+GiJNxKZNSigh5sNgEhzo+SQxKCD5cQ+2VgdlFm+kwVqSonFzRh1R69MVGjuCdLR6zzw 0R+zwJ6Za5FHNjE5l4rJhzKvnlp+KHQsfjYu2jMNRfUcuK3V4wQDDfovU8sNJ+9WxxycQC5g U1jMnHDWq5ViLxjM2tsjV2F0XOqMftVUa0CYAVCnZmq
Ironport-sdr: 646b3bb5_N01pMZK2U8yAAUJdrh4PZWSHk7QtNlfIFAO1+YjfWx9F3qv HmJtRgg4Clc3W60tdRNrwumPFNXBWxOK1xNtACA==

pet, 19. svi 2023. u 18:46 mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> napisao je:

that functions that computes fuel were alway primitive recursive, but
it may or may not be the case.

You still sound too indeterminate about it. In fact the equivalence holds: a recursive function is primitive recursive if and only if its number of calculation steps is bounded above by a primitive recursive "fuel" function.

Vedran Čačić

[Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function, mukesh tiwari, 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, 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