Talk:Pure type system/Archive 1

Archive 1

removal of cite

I restored a reference to the article that I added a few days ago [1] and which Kaustuv removed a few hours later on NOR and COI grounds.[2] I felt the addition was worthwhile since the cited thesis contains some very good exposition of the existing literature and a good reference list [3] in addition to describing some implementation work bringing this theoretical topic closer to practical interest.

According to Google Scholar, contrary to Kaustuv's edit summary, the extended abstract in the linked page has been cited by 5 published works that are not self-cites.[4] I recognize the authors of a couple of them as well-known names in the field. Roorda's thesis itself is not cited in other works since it is a masters' thesis and (unlike a PhD thesis) its main purpose is to demonstrate familiarity with existing work in the subject area rather than to present new results for re-use by others. My main purpose in linking to it was for its expositional content, as is appropriate for an encyclopedia article.

COI definitely does not apply since I have nothing to do with the authors of the cited work. NOR does not apply since there is no attempt to insert any original research into the article. While Roorda's thesis does contain some new research contributions, it is an academic thesis done under the supervision of a well known professor in the field and accepted by the department, and in that sense it has undergone review. I believe that the cite meets all the positive recommendations of Wikipedia's external link policy WP:EL and doesn't run afoul of any of the negative ones. The author later did a PhD in a somewhat-related topic and is now a researcher in a respected university department.[5]

I thank Kaustuv for creating this article in the first place but I think he is being overprotective of it (WP:OWN). The subject area is a respectable but somewhat obscure academic topic on the boundary between theoretical computer science and mathematical logic. It's not a fringe topic that attracts much flakiness or self-promoters. There is not any controversy that I know of regarding the content of the cited work. The various policies Kaustuv cites are the result of endless disputes in Wikipedia areas related to politics, living persons, commercial products, etc, and the policies are needed to beat back tendentious or promotional editing in those areas (and occasionally elsewhere). But in these more serene academic topics like pure type systems, it's best to apply common-sense editorial judgement about the relevance and quality of external cites, rather than bringing out policy machinery that was intended for a completely different purpose. As such, it's best to discuss this type of citation on the basis of whether it improves the article, which in this case I think it does. 207.241.239.70 (talk) 04:50, 21 November 2008 (UTC)

Problems with redirection for this article

What is going on? The article contains links to Girard's paradox and L-cube. If you click these links, they are redirected back to this page. Would be great if this could be fixed.

Vlad Patryshev (talk) 02:20, 4 October 2009 (UTC)

The last paragraph needs rewording?

The last paragraph asserts an implication (not strongly normalizing implies not weakly normalizing), and then states that the contrapositive (weakly normalizing implies strongly normalizing) of that implication is an open problem:

Furthermore, all pure type systems that are not strongly normalizing are not even (weakly) normalizing: they contain expressions that do not have normal forms, just like the untyped lambda calculus. It is a major open problem in the field whether this is always the case, i.e. whether a (weakly) normalizing PTS always has the strong normalization property.

Maybe the original assertion is supposed to be weakened to "all known examples"? Enoksrd (talk) 01:18, 8 November 2010 (UTC)

I had the same impression. 86.6.29.23 (talk) 11:06, 29 November 2011 (UTC)

context-setting

The phrase

In proof theory and type theory,

obviously does nothing to tell the lay reader that mathematical logic, rather than, for example, biology or theology, is what this article is about, nor would they have learned that from the first paragraph.

I've edited accordingly. Michael Hardy (talk) 02:01, 22 May 2011 (UTC)

Archive 1