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: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Turning Non-Primitive Recursive Function into Primitive Recursive Function
Date: Mon, 22 May 2023 18:46:52 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f169.google.com
Ironport-data: A9a23:IO4CwqnCkZTer9Wgn9cmFbzo5gxfIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIeWW2GbKvcZjSjKtskPt+w9kwP7JSDztQ2HgU9/io9RVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajp8B56r8ks156yv4mlA5zTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1xNWgtEtdAp9pxQnAR8 /5bBGomRyG60rfeLLKTEoGAh+wmJcjveYcd4zRulG+IS/khRp/HTuPB4towMDUY3JgfW6aDI ZBBOXw2MkWojx5nYj/7DLo7geSlnXnjciJRslPTpKs2/237wwl40byrO93QEjCPbZwNzx/A/ DufowwVBDkTKITAlh/VtU6Jg7HBx37LdpAWK6yBo6sCbFq7nzRPUnX6T2CTqv6gz0W6Rth3M F0R4iNorK4o9UXtQMOVYvGjiHuNvxpZX9gJVuNjtlDLxa3T7AKUQGMDS1atdeDKqucpfBUx+ QXRwu/vRi0wtr/WZSi234at+Gba1TcuEUcOYioNTA0g6tbloZ0ugh+ncjqFOP7l5jESMWGgq w1mvBTSlJ1I0pFWj/TTEUTvxmPz9sKQH2bZ8y2OBjr9hj6VcrJJcGBB1LQ2xfNJLYLcSlvY+ XZdxZnY4+cJApWA0ieKRY3h/Y1FBd7Va1UwYnY1R/HNEghBHVb9J+i8BxkgeC9U3j4sI2OBX aMqkVo5CGVvFHWrd7RrRIm6Ft4ny6Ptffy8CKCIMIsVMsIuK17ZlM2LWaJ29zC9+KTLufFvU ap3je7xZZrnIf42l2buHLt1PUEDmnpnmAs/uqwXPzz+iebEDJJkYbgCN1SKY4gEAFCs8W3oH yJkH5LSkX13CbWgCgGOqNJ7BQ5QcRATW8utw+QJLb7rH+aTMDt+YxMn6ehxJdINcmU8vrugw 0xRrWcBlwem1COfcl7XAp2hAZu2NatCQbsAFXREFT6VN7ILOO5DNY9OLMdlTqpt7+F50/9/Q t8MfsjKULwFSS3K935ZJdPxpZBrPkbjzw+fHTuXUB5mdb5ZRivN5oDFeCnr/3IwFSaZj5Y1j ICh8QL5eqA9YTpeIvzYU9+R6m+gnGM8nbtyVnTYI9MId0TL9pNrGhPLjfQ2Ap8tLEzDzwSFy wy5Bgc8mtjdhY027euT1L629ZetN+5YAEBhPnL66IyuPnLw5VuTwo5nUceJcwvCVWjyxr6QW OVNw9z4M9wFhFxvoaMmN5pKlIUQv8DOoZ1exSRaRET7VUyhUO5cEyPXzPtxub1o7Z4HnwmPA 2ak2MRQYJeNM+PbSG8hHhIvNLm/5KtFiwvpzKoHJWvh73VK55uBa0JZOieMhAF7LLdYNIAEw /8riPUJ6j6Q2wYbDdKbsh96r2i8DGQMc6EChKEoBIXGjgkKyFYbb6fMVQ7wwpWEMOtXPmcQf zS7uavlhpZn/HTkTUYdL3b34Lditcw8gywSlF4mDHaVq+XBnc4yjUFw8yxobwF7zSdn8uNUO 0ptPXJbPa+lojVi3pBCe0uOGAhxIgKT1WKs6lkOlUzfF1KJUE6UJkIDGO+9xmIr2EMCQSp6p Zaz13TAfQvxWv3Izg8eeBJAuuPya95c7SjAk52XJNuEFJwEfjbVuK+iSm4WoR/BA8lqpkn4i cR13eR3e4vpHDUxpvAlNoykyrggchCIC2hcS/VH/qlSP2X9eim36AeeOXKKZcJBCPzbw3CWU /U0CJp0aC2/8yKSohQwJ60GeeZ0lcF0wusyQOrgIGpevoaPqjZsjonryRH/o20VEvFOisc2L 73Dew2SSlKwgWRmoE6Tjc1mFFfhX/w6Slzd5s6X/t8NNao/i8B3UERr0rKLr3SfawRm2BSPv TL8Xazdzs086IFgg7rTFr5nAiOqI+jST8WNyhi46P5VXOPMMODPlgIbkUbmNAJoJoksW8x7u LCOkdzv1mbHgeoSf0XGvaKeTo9lyN6XXuVFFu7WdlxhgjqkSsvgxzAh6lKIA8VFv/0F7/b2W jbiTtW7cOAkfut0xVpXTnN7OAkcAaGmVZXQj3qxgNrUAydMzDGdCs2s8ELoSmRpdiUoHZnaI S2sstaM4uFolqh9NCUmNdpHXaAheETCXJE4feLfrTObV2mkom2Ts4vYyCYP12v5NWmmIu3bv 7T1HxTwTUHn8uWAhtRUqJd7sRArHW5wy7t4NF4U/9ltzSu2FigaJOAaKo8LEYxQjje07pzje TXRdyE3PE0Rh9ifncnUu7wPnztzB9Di/v/8Lz0tukeWMmK4Xd3RRrRm8Shk7jF9fT6LICRL7 z0B0iWYA/Rz6sgBqSUvCjiTjuJux/eczXUNkaw4u9KnGA4QWN3my1Q4dDeglkX7/wXlm0DCJ GxzTmdBKK1+pYgdDu44E0No9NolUP8DAtnmgepjADoShmlD8NB99Q==
Ironport-hdrordr: A9a23:Bdk2Za/q+n0z8Te7Itduk+DnI+orL9Y04lQ7vn2ZLiYlCvBw9v re5cjzsCWftN9/YgBEpTntAtjjfZqYz+8X3WBzB9aftWvdyQ+VxehZhOOI/9SjIU3DH4VmpM BdmsZFebvN5JtB4foSIjPULz/t+ra6GWmT69vj8w==
Ironport-phdr: A9a23:EFfRvBBnUTEU6+C6vVhIUyQUzEkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8wygSWBM6Hu7ptsKn/jePJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNYwhEnjSwbLFvI Bm5ogjctdQdjJd/JKo21hbGrXxEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2V KRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+4 6t3ThLjlSEKPCM7/m7KkMx9lK1UoByjqBJ/zYDaY5ybOuRica3SZt4aWXNBU9xNWyBdHo+xb Y0CBPcBM+ZCqIn9okMDrR6jBQmvGuzv0T9IjWLq3a073eUuCxvG3A09FN8JtXTUsdb1O7kJU eC10KnIzDvCYOlM2Tf88oTIcxEhofCQXbJ1asfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFvW v6hhXQ9pAFtvjig2N0sio/Ri4wby13J6CF0zYI3KNC5RkN2fdqpHZVRuiybNoZ7RswsTW52t ComyLAKpJy2cSoJxZonxxPTdf+KfoaI7BzjVuucJypzinF9eL+nmRq+7Uytxvf/W8S0ylpGs DZJn9rWunwQ1hHe7s6KQeZn8Ei7wzaAzQXT5/lEIU8qkarbLIYswrsqmZoStUTPByv2mEfrg KOPeEUo5+ml5uD9brXpoZ+cMIB0igXgPag0hsO/BuE4PhAPX2id5+u8yKXu8VPlTLhOlPE7k anUvIrEKcgHpaO1GRJZ34cn5hqnCjepytUYnX0JLFJffxKHipDkO1TTIPD7E/i/mFSskCtqx /HIJLLhGJTNImLCkLfgfLZ990tcxRE8zdBa/Z1UC7UBLOjvVU/2sdzUFhk5PBeszOb9FNp9z p8eWX6IAqKBLa/eqUWI6f43I+mQeI8Vvy7wJOQi5/73lHM2hVsdfbSy0pYMc3C5HvFmI12Db nb2g9cBF30KvgskQ+Dwhl2CS20bW3HnVKUlozo/FYiODIHZR4nrjqbS8j28G8hTe2NLEVDED Xb3fp+FE6MJdSGfOc99kyMNT7nnSo4gyRSGuwrzyr4hJe3RrH5L/an/3cR4srWA3So58iZ5W pz1OwClSmh1mjlNXDoqxOVlpkc7zF6f0K9+ivgeFNpJ5voPXB1pfYXEwblcDNb/EhnEYs/PU EyvF9C7AjwqTs4w3NYUYgB8GtS+izjM2iOrB/kekLnYTIcs/Pfk1mPqb914126A0aAgi1c8R c4aMHCli7V/6wnMDpTI1USYlrqvXasZ1S/JsmyEyDnGp1lWBSh3V6iNRnUDfg3WoND+s1vFV KOrAK87PxFpzMeDLu5OaISsgwwYFbHsP9PRZ2/3kGC1bfqR7pWLaoeiO2AU3SGHTVMBjxhW5 3GNcw43GiampWvaSj1oD1PmJU32o6F4rzugQ0k4whvvDQUp3qep+hMTmf2XSu8ClrMCtiA7r jxoHVG7l9vIAtuErgBlce1Se9Q4qFtA0GvYsUR6MPnCZ+hnm10TaARrvlznzRQxC4RBjc0Co 3YjzQ40IqWdkRtAez6ewZHsK+jPMGChmXLnI6XS21zYzJOX4vJVsKV++wil5ln5UBN8oiYCs ZEdyXaX65TUARBHVJvwVhxy7B1mv/TAZSJ74YrI1HpqOK3ysznY2ttvCvF2r3ToN9pZLq6AE xf/VsMAAM37Yuk3mFWybg4FI+lI9eg1PsK6ctOJ3aeqOKBrmzfs3gElqMhtl1mB8SZxULuC2 osGzuqYwgqYXi39ylags9zysY9BbDAWWGG4zGK3YewZLr03doENB2C0JsSxzdgrnJ/hVUlT8 1u7Dk8H0sukEfaLR2T0xhYYlUEeoHj93DC90yQxiTYi6KyWwC3Jxe3mMhsBIG9CAmd43x/gJ o29jtZSW0bNDUBhkQam6F3626lErb5+aWjSQFtNVyfzJmBmFKC3s/KObtVO55UhrShMGL7kM BbKF/in+0tcin2yV2JFoVJzPymnoJD4gwB3hCqGIXB/oWCYMcB8yBHD5cDNEPtY3z4IXi592 ly1ThC3O9ik+8nRlo+W6LjvETL8EMcLIW+yk9LT0UnzrXdnChC+gf2pz9juEAxglDT+y8EvT yLD6hD1fojs0a2+d+NhZEhhQlHmuK8YUslzlJU9gJYI1D0UnJKQqDACjGT+KtVH2L33dntLR D8K39v97w3s2UklJXWMjdGcND3V0o56at+2b3lDkCcg7M1RCLuV87VenG10o1ukqCreZPF8m nEWzv5kuxt4y6kZ/QEqyCuaGLUbG0JVaDftmxq/5Ne7tKxLZWyrfOv4xA9kkNumFr3HvhBEV SOzZMI5BSEppJYaUhqEwDjp54rjYtWVcd8DqkjejULbl+YMYJMpyqhR2Gw+aDq75yF6jbZ81 0Am3Inm7tbbbT82p+TgXEYebnqsNqZxsnnslfoMwJjQhtj1WM0nQnJRBNPpVa76TmxU76i2c VbWVmV78C/TGKKDT1DFrh466SueSdbzcCjHQRtRhdR6GEvCeAoG2l1SBHNi2cdnXgGymJ64K Bc/v29OoA6+8lwWk6ppL0WtCziE4l75NnFsDsDYdUQzjEkK5l+JY5bGv6QjQmcBpM3n9EvUd SSaf1gaVzhXHBHUQQmyZP/2ooCRu+mAWrjkdqWIO+7f77cEEa/PnMPKsMMu6T+IMo/n0mBKK fo91wIDWHl4H56cgDATU2kNkCmLaceHpRC68ykxr8al8f2tVhi9rY2IQ6BfN9li4XXUye+KK vKQiSBlKD1ZyoJExHnGz6Ia1UITjCcmfiekELAJvyrABKzKnaofAxkeYiJ1fMxGisB0lhFKI tLeg8jp26RQi/c0DxJBVwWklJj3NIoFJGayMF6BD0GOdfyHKTDN38DrcPa8RLlX34A2/1W7v TeWFVOmPyzWzWG4EUDyd7sU3GfCYk0N3eP1OgxgAmXiUt/8PxiyMdstyCYz3aVxnHTBc2gVL Tl7dUpJ6LyW9yJRxPtlSAkjpjJoK/eJnyGB4qzWMJET5LFuHyd5jOJG4Wsz0boT7SBFWPldl y7br9ooqFaj2LrqqHIvQF9VpzBHiZje911lIrnc/4JcVGzs+RsM6SCUCU1PqYI7W5vgvKdfz tWJn6X2YmQnkZqc7Y4XAM7aL9iCOXwqPE/yGTLaOwACSCaiKWDVg0E1eBC683SUqt0+qMGpl sNQG/lUU1s6Ev5cAUNgToRqyHhfUTYtkLrdh8kNtyPWRPz5S8BTv5SBXfWXU62HFQ==
Ironport-sdr: 646baa97_+1e86EPzDbPLcPqbsmx9ymoRjeafhRUBHcY0SywzFTDfT9K 7BlAvAdfeu5z0fNL1xIVtqqYePJXyTX1HyBGrvQ==

> 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.

Thank you, Vedran!

Best,
Mukesh

>
> --
> 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