X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week1.mdwn;h=0122ed9bcc774f3252284ee649498aae6e353fe6;hp=c68da8a0e636b1ceba1cdfbf955905168ee076dc;hb=08ddabea126b05d49bd952365760d322bcae0304;hpb=87483b8ff52adf85fd8d80060427f9e67f698b8a;ds=sidebyside diff --git a/week1.mdwn b/week1.mdwn index c68da8a0..0122ed9b 100644 --- a/week1.mdwn +++ b/week1.mdwn @@ -99,6 +99,30 @@ For the most part, these uses are only loosely connected to each other. We'll te Map === + + + + + + + + + + + +
Scheme (functional part)OCaml (functional part)C, Java, Pasval
+Scheme (imperative part)
+OCaml (imperative part)
lambda calculus
+combinatorial logic
--------- Turing complete ---------
  +more advanced type systems, such as polymorphic types +  +
  +simply-typed lambda calculus (what linguists mostly use) +  +
+ + + Rosetta Stone ============= @@ -281,14 +305,14 @@ Lambda terms represent functions All (recursively computable) functions can be represented by lambda terms (the untyped lambda calculus is Turing complete). For some lambda terms, it is easy to see what function they represent: -(\x x) represents the identity function: given any argument M, this function -simply returns M: ((\x x) M) ~~> M. +> `(\x x)` represents the identity function: given any argument `M`, this function +simply returns `M`: `((\x x) M) ~~> M`. -(\x (x x)) duplicates its argument: -((\x (x x)) M) ~~> (M M) +> `(\x (x x))` duplicates its argument: +`((\x (x x)) M) ~~> (M M)` -(\x (\y x)) throws away its second argument: -(((\x (\y x)) M) N) ~~> M +> `(\x (\y x))` throws away its second argument: +`(((\x (\y x)) M) N) ~~> M` and so on. @@ -309,13 +333,11 @@ both represent the same function, the identity function. However, we said above (\z z) -yet when applied to any argument M, all of these will always return M. So they have the same extension. It's also true, though you may not yet be in a position to see, that no other argument can differentiate between them when they're supplied as an argument to it. However, these expressions are all syntactically distinct. +yet when applied to any argument M, all of these will always return M. So they have the same extension. It's also true, though you may not yet be in a position to see, that no other function can differentiate between them when they're supplied as an argument to it. However, these expressions are all syntactically distinct. The first two expressions are *convertible*: in particular the first reduces to the second. So they can be regarded as proof-theoretically equivalent even though they're not syntactically identical. However, the proof theory we've given so far doesn't permit you to reduce the second expression to the third. So these lambda expressions are non-equivalent. -There's an extension of the proof-theory we've presented so far which does permit this further move. And in that extended proof theory, all computable functions with the same extension do turn out to be equivalent (convertible). However, at that point, we still won't be working with the traditional mathematical notion of a function as a set of ordered pairs. One reason is that the latter but not the former permits uncomputable functions. A second reason is that the latter but not the former prohibits functions from applying to themselves. We discussed this some at the end of seminar (and further discussion is best pursued in person). - - +There's an extension of the proof-theory we've presented so far which does permit this further move. And in that extended proof theory, all computable functions with the same extension do turn out to be equivalent (convertible). However, at that point, we still won't be working with the traditional mathematical notion of a function as a set of ordered pairs. One reason is that the latter but not the former permits uncomputable functions. A second reason is that the latter but not the former prohibits functions from applying to themselves. We discussed this some at the end of Monday's meeting (and further discussion is best pursued in person). @@ -325,7 +347,11 @@ Booleans and pairs Our definition of these is reviewed in [[Assignment1]]. - +It's possible to do the assignment without using a Scheme interpreter, however +you should take this opportunity to [get Scheme installed on your +computer](/how_to_get_the_programming_languages_running_on_your_computer), and +[get started learning Scheme](/learning_scheme). It will help you test out +proposed answers to the assignment.