From 4d9fe4645917a4966694c7c4bf8edde8b243745f Mon Sep 17 00:00:00 2001 From: Chris Date: Thu, 26 Feb 2015 13:15:13 -0500 Subject: [PATCH] edits --- topics/_week5_system_F.mdwn | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index 4bde11e0..0dcb0957 100644 --- a/topics/_week5_system_F.mdwn +++ b/topics/_week5_system_F.mdwn @@ -9,23 +9,6 @@ simply-typed lambda calculus as a way of expressing natural language meaning. So we will need to get more sophisticated about types. The next step in that journey will be to consider System F. -In the simply-typed lambda calculus, we write types like σ --> τ. This looks like logical implication. We'll take -that resemblance seriously when we discuss the Curry-Howard -correspondence. In the meantime, note that types respect modus -ponens: - -
-Expression    Type      Implication
------------------------------------
-fn            α -> β    α ⊃ β
-arg           α         α
-------        ------    --------
-(fn arg)      β         β
-
- -The implication in the right-hand column is modus ponens, of course. - System F was discovered by Girard (the same guy who invented Linear Logic), but it was independently proposed around the same time by Reynolds, who called his version the *polymorphic lambda calculus*. -- 2.11.0