Talk:System F

Older comments

I tried to add a reference to the use of system F in GP. The process to cite is opaque and I don't get it. I don't have time to go through the 5 pages of documentation that are on the site (not one of which even contains a simple example that I can just reuse). —Preceding unsigned comment added by 205.193.82.252 (talk) 16:25, 3 April 2009 (UTC)

---

It says in this article that there are several ways to define natural numbers in the typed lambda calculus but I have only seen church numerals and variants on that theme. A natural number is zero or a successor of a natural number: and the same structure is forced by giving a formula the type (a -> (a -> a) -> a). Alternatives would be welcome, of course. (though this is probably off topic) 69.181.45.120 15:57, 10 December 2005 (UTC)

Barendregt's system maybe, haven't seen it used outside of untyped, but I see no reason it can't be used in System-F. Rajakhr (talk) 03:37, 6 April 2010 (UTC)

---

This article should contain a note about Turing completeness (or the lack thereof) since said article links here. 82.139.85.127 00:00, 8 February 2007 (UTC)

System-F is strongly normalizing and thus not turing complete. Rajakhr (talk) 03:37, 6 April 2010 (UTC)

---

It's a bit confusing / inaccurate to say that System F corresponds to "second-order logic", primarily because there are many second-order logics. It would at least be more precise to say that System F corresponds to a second-order intuinistic propositional calculus. "Second-order logic" on its own could mean, e.g., intuinistic second-order logic with quantifiers, which corresponds to the Calculus of Constructions / Lambda P omega. (This is because types parametrised by terms (i.e., dependent types) are required to represent formulae of the form "forall x : A . P(x)" where A is some type, x is an object in A, and P is a function from A to proposition (i.e., a predicate on A); this formula corresponds to the type "(Pi x : A) P[x]".). —Preceding unsigned comment added by 99.133.187.65 (talk) 14:57, 2 May 2008 (UTC)

---

Why isn't there a citation to John Reynolds's work on System F? Norman Ramsey (talk) 04:31, 12 February 2010 (UTC)

Added citations to Reynolds & Girard. Noamz (talk) 20:20, 6 April 2010 (UTC)

Etymology

According to a comment posted by Dr. Charles Stewart on a thread at Lambda-the-Ultimate on 2008-10-20: "Look at the introduction (pp2-12) of Girard's thesis, Interpretation fonctionnelle et elimination des coupures de l'arithmetique d'ordre superieur (PDF: fragment only), where the term [System F] is introduced by explicit contrast to Gödel's System T, which —being Girard— he doesn't refer to System T there directly as such but as "le système de Gödel OF_1", ie. the order-functional-one system of Gödel. I have heard that Girard delights in the carefully obscure, but I think this is where System F is named. For completeness sake, Gödel described his System T in his 1958 Dialectica paper, which was later translated into english under the title On a Hitherto Unexploited Extension of the Finitary Standpoint. I have the idea that the T stands for "type", as in "primitive recursive functionals of finite type", cf. Avigad & Feferman's Gödel’s Functional (“Dialectica”) Interpretation, although, as for F, I am not quite sure." --Omnipaedista (talk) 23:28, 14 June 2011 (UTC)

Bob Harper explains in a lecture on the Principles of Programming Languages that he thinks the F is a play on booleans, which are sometimes shortened to T and F for true and false. --D!mens!on (talk) 14:58, 22 February 2022 (UTC)

Boolean in some formulae

As far as I can tell, the non-superscript occurrences of "Boolean" in the definitions of e.g. AND, i.e.,

$\mathrm {AND} =\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,y\,\mathbf {F}$

are (i) undefined notation (type where a term would be expected) and (ii) not necessary, in the sense that

$\mathrm {AND} =\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,y\,\mathbf {F}$

should be a sufficient and correct definition. I may however be missing something subtle. 130.239.128.243 (talk) 15:17, 7 October 2011 (UTC)

Those occurrences of ${\mathsf {Boolean}}$ occurring within the lambda expressions would actually be necessary. Any universal quantification of a type variable in the type of an expression means that the expression needs to be "fed in" an extra argument which specifies a type; a "type expression", if you will. That type argument is bound by that "big lambda" at the beginning of the expressions for T and F; i.e., the fed in "type expression" is bound to a type variable. ${\mathsf {Boolean}}$ would be a meta-symbol (outside of the System F itself) which is shorthand for the "type expression" $\forall \alpha :\alpha \rightarrow \alpha \rightarrow \alpha$. —AugPi _(t) 18:18, 14 July 2012 (UTC)

In the definition of $\mathrm {AND}$, x is of type ${\mathsf {Boolean}}$ which means that x would require three — not two — parameters; the first parameter being a "type expression", and the next two parameters being lambda expressions. (That should become clear by looking at the definitions of both T and F; both are lambda expressions which have three lambdas, not two; the first lambda being big. Also, T and F should be the only possible expressions of type ${\mathsf {Boolean}}$; after a type is fed to such "Boolean", two values of that type are fed to it, and then a value of that type is expected as output. An arbitrary constant output could not be returned because it might easily not correspond to the required type (fed in at the beginning), which leaves basically just two choices for output: either the second or the third parameter, both of which have the required type.) —AugPi _(t) 18:32, 14 July 2012 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified 2 external links on System F. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Corrected formatting/usage for http://www.church-project.org/reports/Wells%3AAPAL-1999-v98-no-note.html
• Added archive https://web.archive.org/web/20140917015759/http://www.eecs.harvard.edu/~greg/cs256sp2005/lec16.txt to http://www.eecs.harvard.edu/~greg/cs256sp2005/lec16.txt

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 18:03, 8 September 2017 (UTC)