most recent 30 from http://mathoverflow.net 2013-05-25T21:46:54Z http://mathoverflow.net/feeds/question/23032 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system Matthew Willis 2010-04-29T19:56:34Z 2011-01-29T18:55:35Z

<p>The systems of the &lambda;-cube have the axiom $\star:\square$.</p> <p>I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\square$ in each interpretation?</p> <p>$t : T : \star : \square$</p> <p><strong>Programs:</strong> t is a program of type T. (Possibility: T is a program of type $\star$?)</p> <p><strong>Proofs:</strong> t is a proof of theorem T. It's hard to see T as a proof of $\star$, though.</p> <p><strong>Set elements:</strong> t is a member of set T. (Possibility: T is a member of the universe $\star$ of sets. Then it seems difficult to assign a meaning to $\square$ that avoids the membership $\square : \star$.)</p> <p>I'd like to fill out this table both vertically and horizontally, with both further interpretations and the missing descriptions of $\star$ and $\square$, and possibly meanings of $T : \square$ for $T \neq \star$.</p> <p>Thank you!</p>

http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/23044#23044 Jacques Carette 2010-04-29T21:40:46Z 2010-04-30T14:23:21Z

<p>$\star$ is a <em>kind</em>, which classifies <em>types</em>. $\square$ is a sort, and it classifies <em>kinds</em>. So this is a 4-layer deep classification. Once you get to have type-constructors, kinds get really useful. Eventually, you wish for kind-constructors too, and then you need sorts.</p> <p>Turns out that you really rarely ever need to get deeper than that (even though Coq and Agda have infinitely many such levels). I am not sure I have ever read a good Curry-Howard explanation of kinds and sorts. I would hazard a guess that classical mathematics rarely worries about kinds/sorts, I would tend to dig into $n$-categories to find a good relation.</p>

http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/23045#23045 Antonio E. Porreca 2010-04-29T21:49:48Z 2010-04-29T21:49:48Z

<p>I seem to recall there’s a really good explanation of kinds and sorts in Sørensen and Urzyczyn’s <a href="http://www.amazon.com/Lectures-Curry-Howard-Isomorphism-Foundations-Mathematics/dp/0444520775/" rel="nofollow">Lectures on the Curry-Howard Isomorphism</a> (a previous version is available <a href="http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf" rel="nofollow">online</a>).</p>

http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/48220#48220 none 2010-12-03T20:56:17Z 2010-12-03T20:56:17Z

<p>I found J. W. Roorda's masters thesis to be a good exposition of PTS. It is linked from here:</p> <p><a href="http://people.cs.uu.nl/johanj/MSc/jwroorda/" rel="nofollow">http://people.cs.uu.nl/johanj/MSc/jwroorda/</a></p>

http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/53733#53733 robin-adams 2011-01-29T18:55:35Z 2011-01-29T18:55:35Z

<p>I've found you won't go far wrong if you think of the objects in * as sets, and the objects in $\Box$ as proper classes. Thus, * is the proper class of all sets.</p>