From 4cc40e4c5ca2646b579213ee40f2caa794a3a474 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sun, 24 Oct 2010 22:12:16 -0400 Subject: [PATCH] added Curry-Howard --- week6.mdwn | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/week6.mdwn b/week6.mdwn index 79b12f71..5f225d36 100644 --- a/week6.mdwn +++ b/week6.mdwn @@ -174,7 +174,7 @@ execution. In Scheme parlance, functions on the unit type are called Curry-Howard, take 1 -------------------- -We will returnto the Curry-Howard correspondence a number of times +We will return to the Curry-Howard correspondence a number of times during this course. It expresses a deep connection between logic, types, and computation. Today we'll discuss how the simply-typed lambda calculus corresponds to intuitionistic logic. This naturally @@ -186,9 +186,9 @@ ground types, a set of functional types, and some typing rules, given roughly as follows: If a variable `x` has type σ and term `M` has type τ, then -the abstract `\xM` has type `σ --> τ`. +the abstract `\xM` has type σ `-->` τ. -If a term `M` has type `σ --> &tau`, and a term `N` has type +If a term `M` has type σ `-->` &tau, and a term `N` has type σ, then the application `MN` has type τ. These rules are clearly obverses of one another: the functional types -- 2.11.0