coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a question about "arities"

From: "William J. Bowman" <wjb AT williamjbowman.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] a question about "arities"
Date: Thu, 17 May 2018 17:20:40 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=wjb AT williamjbowman.com; spf=Pass smtp.mailfrom=wjb AT williamjbowman.com; spf=Pass smtp.helo=postmaster AT williamjbowman.com
Ironport-phdr: 9a23:zz8GNBBV2yz7cCfu25a5UyQJP3N1i/DPJgcQr6AfoPdwSPvzo8bcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJKjA5/mHLhcJ3jq1VoxyvqQJwzYHbe4yVKON+fqbBcdMaWWZMXMBcXDFBDIOmaIsPCvIMMehYoIn8o1sOqRq+ChOpBOjyzjFEnGL90LA90+UvFAHJxgogE9wTu3nTotT1NrwdXPu7zanJyTXDa/JW1i346IjKaR8hpv+NXbdqfsrX00UgCwTFjlCJpIHjIjib2OMNs22B4OphU+Kik28nqwdrojiu3MggkIfJhpgTx1vZ9it52J44KcC8RUJle9KoDZtduiGAO4Z1Qc4uWXxktDs7x7EepJK2eDYGxI4lyhPecfCLboeF7xP5WOuRPDt1gm9udqiliBao60egz/XxVsmq31ZOqSpIitfNtnEJ1xzX68iIUP59/kW61jaI2QHT7/tLIUYumaXHLJ4hx6Y8lpsVsUvdAi/7gFj6gauIekk+5+Sl6+Tqbq/lq5KfLYN4lxzyP6U2lsy6G+s4MwwOX2aB+eS70b3u5UP4QLdRgfAtnKjZsZTaJcAapqGjBg9V0J0s6xGxDjejytsYm2MLI05CeBKCl4TpIU3BIOjkDfejhFShiCtkx/ffPrH4HprNKmXDn6z6cLZm609czRIzwspF65JVDLEBOvPzVVXruNzWFB9qezCzlu3gEZB20p4UcWOJGK6Qdq3I4nGS4ed6adaNYIsUsTO1Cb5tzfnxiHY/0xdJYquj9YQWbHS5F/FkKUKGZHPqxNwGFDFZ7UIFUOX2hQjaAnZobHGoUvdkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzoeWE+NFXPpfoCGUfATbSuUZMRml25dDOTze8oazRir8TTC5f9/NOOOon8HtJbn1dFw5efUihQ783p/CMHPizjQHVExpXsBQnoN5I46oUF5zQ3bg7d5h/hZHNlR7fRWVw48c5Xbyr4jBg==

The term comes from (or at least dates back to) "Codifying guarded
definitions with recursive schemes". The way I think of this is these are the
"arities" of constructors in the sense that they tell you how many and what
types of arguments constructors take.

--
Sent from my phoneamajig

> On May 17, 2018, at 14:35, Matej Košík
> <mail AT matej-kosik.net>
> wrote:
>
> Hi,
>
> The Coq Reference manual (in the section about CIC)
> https://coq.inria.fr/refman/language/cic.html#well-formed-inductive-definitions
> defines these concepts:
>
> - arity of a given sort
> - arity
>
> The concepts is essential, but what I don't fully understand is why we
> refer to these concepts as "arities".
> Does it make sense to overload the existing meaning of the word "arity"
> more than overloading the meaning of some other word?
> Do some other communities use this word in the same way as the Coq
> community does?
> What is the point?
>
> Does anybody has a clue?

[Coq-Club] a question about "arities", Matej Košík, 05/17/2018
- Re: [Coq-Club] a question about "arities", William J. Bowman, 05/17/2018