Home » forums » LtU Forum

F in System F

What does the F stand for in System F?

Thanks,
Chris

By christopher at 2008-10-19 17:06 | LtU Forum | previous forum topic | next forum topic | other blogs | 6560 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Homework?

Is this a homework problem?

By dmbarbour at Sun, 2008-10-19 17:15 | login or register to post comments

No, this is not a homework

No, this is not a homework problem.

My goal is to prove strong normalization of System F in the Isabelle theorem prover.

However, no description of System F that I have found says what the "F" stands for, and I was just curious.

Chris

By christopher at Sun, 2008-10-19 17:58 | login or register to post comments

Well, I also can't provide

Well, I also can't provide an answer off the top of my head. You may need to look up some papers by John Reynolds or Jean-Yves Girard who both independently developed System F (1974 and 1972 respectively). Reynolds, I know, has written several papers about it.

By dmbarbour at Sun, 2008-10-19 19:16 | login or register to post comments

My guess

It is probably because of the [F]orall quantifier. I checked in Proofs and Types and The Blind Spot and I could not find any explanation there.

By Matthieu Sozeau at Sun, 2008-10-19 19:32 | login or register to post comments

Not a bad guess...

...as System F has to do with universal quantifiers. Other guesses might be Frege (since he had an earlier notion of system F) or Functor (since it has to do with second order logic).

But my best guess would be none of the above. It probably means no more then lambda does. System F was probably just chosen to differentiate itself from Goedel's System T.

By Chris Rathman at Sun, 2008-10-19 20:52 | login or register to post comments

I sent an e-mail to Dr.Reynolds

I sent an e-mail to John Reynolds. Perhaps he'll get back to us with a definitive answer.

By dmbarbour at Sun, 2008-10-19 21:04 | login or register to post comments

Système fonctionnel?

Look at the introduction (pp2-12) of Girard's thesis, Interprètation fonctionnelle et èlimination des coupures de l'arithmètique d'ordre supèrieur [PDF: fragment only], where the term 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.

Postscript: 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.

By Charles Stewart at Mon, 2008-10-20 21:18 | login or register to post comments

Thanks! Just what I was

Thanks! Just what I was looking for.

Chris

By christopher at Tue, 2008-10-21 03:45 | login or register to post comments