Talk:System F

Latest comment: 2 years ago by D!mens!on in topic Etymology

Older comments

edit

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)Reply


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)Reply

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)Reply

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)Reply

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

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)Reply


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

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

Etymology

edit

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)Reply

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)Reply

Boolean in some formulae

edit

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

 

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

 

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)Reply

Those occurrences of   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.   would be a meta-symbol (outside of the System F itself) which is shorthand for the "type expression"  . —AugPi (t) 18:18, 14 July 2012 (UTC)Reply
In the definition of  , x is of type   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  ; 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)Reply
edit

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:

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)Reply