coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Makarius <makarius AT sketis.net>
- To: coq-club AT inria.fr, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
- Subject: Re: [Coq-Club] Why dependent type theory?
- Date: Wed, 4 Mar 2020 10:28:13 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=makarius AT sketis.net; spf=Pass smtp.mailfrom=makarius AT sketis.net; spf=None smtp.helo=postmaster AT relay.yourmailgateway.de
- Autocrypt: addr=makarius AT sketis.net; prefer-encrypt=mutual; keydata= xsFNBFcrF+4BEADMcXMnu3XHg6bRsGe3tajAHqvm89+ecn/Y0WhjI2FplhkZs1LwM+ZA9eXh hiBrC/yX0FJ+qjzVIfm66CX4nzVG1f8qwaervMpvpA+gbhtQiXc0t+LDcqV+5cdtpKplPHSu oW+KzJKyCdkDB5fYMOzuaXQwYi12YAEQH2r6K7Q7Np+k82Xli1pWe+Tha/BH0pKJ5Q01aPep ASrNW9F+moX7C0fxWl65LiXGmF0UJep6fqKruhy8oNF4p6I2oZhktvaR/x6tkL2PkT3r+xUS 6g5i3BOjfwhoGY57nsioeK+8VFvdRH5DK4CbrTgDl7ddcrEeENrfpDiPLs/afVbe/T9oDXmJ OJAO4WMpfZNiFhx9SSVTHohw29Fyzn0N1UQGjPqAY1jg32DAxlnMQ0co/KabEFAcoQsW1/6U ZGiNxYVIyEKGrnSY4WuLuNC8CmU1RaYSdTk1y9tYdxufM9lH9ynzJwac6FdalOOxMR2G9JG8 L9/dk3ytlP6DVwkPBSCpJaTkTyMp1wSkF1oK/BDu5xKUQh0zvvLCuZ16hiKRBBSjpVExXRZC u+NC1Y4wqm1HOH7HBwgZ1Hv9S/EPmI9iwgcW0SpDJqPf2Cm7oFMZsZ5Dbs6/nOQoe4Zegy45 ymqDRlIekP7zj+vOoR80XAYfmAH5DElJHldcjmgLBMdpvvqGZwARAQABzR5NYWthcml1cyA8 bWFrYXJpdXNAc2tldGlzLm5ldD7CwX0EEwEIACcFAlcrF+4CGyMFCQlmAYAFCwkIBwIGFQgJ CgsCBBYCAwECHgECF4AACgkQ89KUEoG/TbiVrw/9FjEBgh2CB7Qof7Y4k0yc7j+x/A0Wmkc0 iwP5jaKJuxRv1JJT8CFqm392+/cdh3EkRUk/UWD+hpNndYJwxZltrEpKVqFAWoVOg3ZJ4cuI MYhlp4tk/T0KSl/gKT16dc6uJ7M/FzW0zv50vjFtAdianEDuqLXHKaGDUwWoOTDly0gdZ7aH /eNby6ONHUSJMdTNOErh2N+uESM4aZqUuuL/dTb6xiVzCpV5saT8EMakoazUd7QhoBaHvqfs BL7DEmvcTtA79GF3ufHrF/UndIcx8aMznZ2PGNjmy5seDCoKX0EYHdLam8vgo/TuU4dRw5Zn 6E/ouyNOliXT1Mn+SomeBSXTR5MXRq4TQ9MKVGiP0Yl+7GJQU0JFtDC1ZZEOyjIiwGWOhbUR pYujVm8C1iQ7NcEn2BqOAmRML6IR6+En4RLbgCNsBNXlmTPRJOaI+iV6DZzg3x9zcaDGhoYt jkBTEFpb0F3jU9yuaEU5401NV34fUxg8tqXs0R9CKinO7kQ8N+RDjyyY8k2KZiDYBJ6r+OK0 d7TaTj7F9tmpAu2pmQ8lxOKjDZIwlbGTsC4lxISmcPzBGTKXja5nakcWYx/lZ4vje0WZ12HN amnD1weakFixRYit0d+Kz7cuj684NSbhwC0oN2t9R06Nfq8UPEWRKEitCly0OtRgio8zVZ/L eADOwU0EVysX7gEQAKs5NVOvYkE/r8KLsJ8/L/9eulpJDOFilZ9fyuqii7t1UpHZLb58QghW JM+IB2GSGsB+pOi6Je7hmwxcVdXYbGlYZ4Btqqw48/XptfbNZ8alCk6AqoVFP4MbYxij/Qqv f/Yw6GR0p1RIC/W4GF/JgDDwDFEiMT6Pv6dpM8acdNFCERDZdoOJiC+XJRwy5lZ2g5FOJkT9 rVI9EnA7mBXLLjPOMUp2/eZxN6gKOZzI3ej9vixg3adWR2yfKPgacHP/ujnVfITOl0OyLE5f zIHq85dEV4zW6Mpx7+Um0tdkwlUVMaW2nQ1bcwejgVAuD/MLSF/lSs3N5D1ctw5QUemYh7/e 2dC12UJuFDFxNPzcltQTlkBCVWV1D0SjScDHdlF6HhzpZOlt52/rwTn5GHtY4nwAL4IJ+Yvl WX8YKmyILH4Ai8c/N2IVRERQ2qorWFlsQnqrXV+hXf8aUwjc/pq4K9rsWxvle3TpeZfoBefU /s1PEX0SepZFAqAXHlQ9DZPsdPDo9EFK695G5w4nf03EhE9TV1MKGUuc1XJ6f1ZLaxu0TwTA 6qYtKIyBcU0Yn61S2Kh7Dgb5LdLV8nfl71+n/xIt2IWH5UJ9YuwEgGEP0c6ImnAUZ+nRodFI 0RwtCWlRkSJWtQln1vcphrz8PjWZH6e/nWnceXR/Al5P0WexQgtvABEBAAHCwWUEGAEIAA8F AlcrF+4CGwwFCQlmAYAACgkQ89KUEoG/Tbh7VQ/9Fc4bdwJYc3jH/LiuXv6uMg50Cv6lg2NT bL9DClWGNiYzejfM2A4c5K+GRUXhyD7S9U203MOv3z7uTbtyQL8XVolNnQlRIkB00f8nJ2sw HMXx/hemjXBvtlneq+vrMORJexldXUMFq19ZZrvj0zZL+pUnGFqt+IWTEE5GpL7wu20Demaj jYyGyKcDZyJOWZcl4e45Yn3hl0EI2xVmVh7ZinVsb3+nqgcltFy4Jt+drezwV2EiLGJHfGsT jEQb3C9VpneU4Jo+hHtfqLK4Q8+WlIOzSfyvwbabxrhyqg7i11fu8yckNW3dCURPYigV07HK 4dN0zhj53M0Q3eTwegJRPJb8XoLDcSdbsaU2HIShlGDKmzS9KL4JzLikQ9dXROC4cae3jRKH aexFi4B55Ab6FxIfXj09wUCO6Nm0owDfIBDMgiywvi2Rb2etCjBgRbSj71S2nntd9ZitoYvE yKirLkWmJRbp3ln8cHi8Uc/jr1cDPVRWuLUN0uceMj5+AR+NZVakcNUHWJCinMMjacho0SyP QmocdU8pzzupreaVWruqaSzqcpWBPwrE5OxEtJ+OyIBjKmRJ5eptjh4rKgNaVnKjhqbvr+Yz pUAgPp38jjf4HJghUGIfWArKNelKJEJOYk94DAbmT67LgqEdZ0yaA2BCHmreN727WIzV9vkX NMc=
- Ironport-phdr: 9a23:yH5W6RGf1kjJyot2/xcGgp1GYnF86YWxBRYc798ds5kLTJ7zoMywAkXT6L1XgUPTWs2DsrQY0raQ6viwEjRaqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi5oAnLq8UanYhvJqktxhfXv3BFZ/lYyWR0KF2cmBrx+t2+94N5/SRKvPIh+c9AUaHkcKk9ULdVEjcoPX0r6cPyrRXMQheB6XUaUmUNjxpHGBPF4w3gXpfwqST1qOxw0zSHMMLsTLA0XTOi77p3SBLtlSwKOSI1/H3Rh8dtl69Qvg6vqAJjzI7VeIGVNeRxfqXBfdMBWGFNWt9dWzFdDo+gaocCCfcKM+RFoInnv1YAsxW+CwmxCu3sxDFHiHD50q8m3OouCgzGwA8tEsgSvHjIotj4NKEfWv21wqnSyjXDautb1zDn54jLaB8hu/CMXa9rccHMzkQvEhnKjlaKpoz/PjOVy/8NvnOA7+pjS+2vl28nqxprrjip2MgslpDEi4QIwV7K8iV5xZw6Jdy+SENjfd6kDZ5QuzuHOIRoRM4pXmJmuD4ix7EbupO2fzIGxZUkyhLFavGLbpKE7g//WOufOTt1hWxpdKihixqv8EWs0PPwWtW73VpQsCZJjtbBu3YQ3BLJ8MeHUOFy/kK51DaPyQ/T7uZELFgulaXFL54u2L4xmoATsETEAy/2gkD2g7WXdkUg9ein8fjnbavop5CGN454kBzxPbo2lsy+B+Q3LBQOUnCG9em/17Dv50z0TbZQgvA3j6XVqo3WKdgVq6KhBg9ayIcj6xKxDze819QYmGEKLFdfdxKElYfpIVDOIO3jDfqkmFSskylkx+zHPr36GJnNKGbMkKv5cbZn90Fc0BYzzcxY559MFr4BJ+vzVlbtu9zcEx82KBe5w/3nCdV4zoMRQ3iDAq6fMKPIsF+H/PgjI+eWZNxdhDGoIP88ovXqkHURmFkHfKDv04FTIFy/G/VgIlyEbDLIi80KEWob+zUzSuDuiVuNGWpfYHOzWaMl+zx9DIu8BofOV8WyjbqN2Ca9EbVSYXpHAxaCCyG7WZ+DXqIpYSGbOM58iXRQULGiQpUgyAqGrwz317t8aOzZ5ntL5trYyNFp6riLxlkJ/jtuApHYijnVFjwmriYzXzYzmZtHjwl9x1OEi/YqmfFcHM0V9vRUSAIzNJrTxvB3FNnjHA7MLI/QFASWB+6+CDR0deofhscUah8nSc6hgwzCxGysDqNHz+XaVqxxybrV2j3KH+g4zn/H0Kc7iFx/GJlUNmC6h7U58QXPVdfE
On 03/03/2020 23:56, Dominique Larchey-Wendling wrote:
> What comes first to my mind is my own experience
> that it is generally not possible to define nested recursive
> functions such as eg MCarthy's F91
>
> F91 x = if x > 100 then x - 10 else F91 (F91 (x+11))
>
> w/o using dependent types because they allow you to express
> properties of the output that you can feed into the type-checker
> for termination.
>
> On the other hand, proving properties after defining the function
> does not work with nested calls because you need those properties
> while constructing termination certificates.
>
> Of course if you work in a framework where termination of all
> functions is not required by the type-checker, then you won't
> have such a constraint.
Indeed. Here is
McCarthy's 91-function in Isabelle/HOL: see "f91" in
https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Functions.html
[This thread now covers 3 mailing lists: Coq, Agda, Lean. Hopefully we won't
see it on isabelle-users or hol-info as well.]
Makarius
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, (continued)
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Mario Carneiro, 03/13/2020
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Kevin Buzzard, 03/13/2020
- Message not available
- Message not available
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Bas Spitters, 03/17/2020
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Thorsten Altenkirch, 03/18/2020
- Re: [Coq-Club] Why dependent type theory?, Guillaume Melquiond, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Dominique Larchey-Wendling, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Pierre Courtieu, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Jeremy Dawson, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Dominique Larchey-Wendling, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Makarius, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Pierre-Marie Pédrot, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Thorsten Altenkirch, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Dominique Unruh, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Jeremy Avigad, 03/04/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Ettore Aldrovandi, 03/04/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Miguel Pagano, 03/05/2020
Archive powered by MHonArc 2.6.18.