From: Jim Date: Thu, 19 Mar 2015 03:36:16 +0000 (-0400) Subject: Merge branch 'master' into working X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=b15a6b392f7989734f899fc9efcb211f95d2f416;hp=f0dac567a643fae66a6cba5b7e85d785c347f2bc Merge branch 'master' into working * master: rename topics/week7__95__combinatory__95__evaluator.mdwn to topics/week7_combinatory_evaluator.mdwn light editing, rename functions for clarity rename topics/week7_eval_combinatory.mdwn to topics/week7__95__combinatory__95__evaluator.mdwn rename eval_combinatory post combinatory evaluator post eval_combinatory rename topics/week7_eval_cl.mdwn to topics/week7_eval_combinatory.mdwn add Plexy and some stubs/reorganization link to Plexy rename topics/_week6_plexy.mdwn to topics/week6_plexy.mdwn update --- diff --git a/content.mdwn b/content.mdwn index b5ecf20f..61ac9611 100644 --- a/content.mdwn +++ b/content.mdwn @@ -7,6 +7,8 @@ week in which they were introduced. * [[What is computation?|topics/week3_what_is_computation]] +* [[Kaplan on Plexy|topics/week6_plexy]] + * Functional Programming * [[Introduction|topics/week1 kapulet intro]] @@ -18,12 +20,16 @@ week in which they were introduced. * More tips on using Scheme * Types in OCaml and Haskell (will be posted soon) * Practical advice for working with OCaml and/or Haskell (will be posted soon) + * [[Kaplan on Plexy|topics/week6_plexy]] and the Maybe type + * Interpreter for Lambda terms + * Starting with Monads * Order, "static versus dynamic" * [[Order in programming languages and natural language|topics/week1 order]] * [[Reduction Strategies and Normal Forms in the Lambda Calculus|topics/week3_evaluation_order]] * [[Unit and its usefulness|topics/week3 unit]] + * [[Combinatory evaluator|topics/week7_combinatory_evaluator]] * The Untyped Lambda Calculus @@ -40,14 +46,19 @@ week in which they were introduced. * [[Reduction Strategies and Normal Forms|topics/week3_evaluation_order]] * [[Fixed point combinators|topics/week4_fixed_point_combinators]] * [[More about fixed point combinators|topics/week4_more_about_fixed_point_combinators]] + * Interpreter for Lambda terms -* [[Combinatory Logic|topics/week3 combinatory logic]] +* Combinatory logic + + * [[Introduction|topics/week3 combinatory logic]] + * [[Combinatory evaluator|topics/week7_combinatory_evaluator]] * Typed Lambda Calculi * [[Simply-typed lambda calculus|topics/week5 simply typed]] (will be updated) * [[System F|topics/week5 system F]] (will be updated) * Types in OCaml and Haskell (will be posted soon) + * Starting with Monads ## Topics by week ## @@ -99,10 +110,17 @@ Week 5: * Practical advice for working with OCaml and/or Haskell (will be posted soon) * [[Homework for weeks 5 and 6|exercises/assignment5]] -Outside readings for week 6: +Week 6: - -* [[footnote about "Plexy"|readings/kaplan-plexy.pdf]] from Kaplan's *Demonstratives* +* [[footnote about "Plexy"|readings/kaplan-plexy.pdf]] from Kaplan's *Demonstratives* about Plexy; [[our notes|topics/week6_plexy]] comparing to the Maybe type * (Recommended) [[King's discussion of Schiffer|readings/king-on-schiffer.pdf]] in Chapter 4 of *The Nature and Structure of Content* (2007) -* Michael Rieppel, "[[Being Something: Properties and Predicative Quantification|readings/rieppel-beingsthg.pdf]]" * (Recommended) [[King's discussion of clausal complements and proposition-designators|readings/king-on-logicism.pdf]] from Chapter 5 of *The Nature and Structure of Content* (2007) +* Michael Rieppel, "[[Being Something: Properties and Predicative Quantification|readings/rieppel-beingsthg.pdf]]" + +Week 7: + +* [[Combinatory evaluator|topics/week7_combinatory_evaluator]] +* Interpreter for Lambda terms +* Starting with Monads + + diff --git a/index.mdwn b/index.mdwn index a764795b..9b6c09c7 100644 --- a/index.mdwn +++ b/index.mdwn @@ -155,6 +155,12 @@ Practical advice for working with OCaml and/or Haskell (all will be posted soon) > We will be discussing the readings posted above. +> Topics: [[Kaplan on Plexy|topics/week6_plexy]]; King on that-clauses and "the proposition that P"; Rieppel on Frege and the concept HORSE + +(**Week 7**) Thursday March 12 + +> Topics: [[Combinatory evaluator|topics/week7_combinatory_evaluator]]; Interpreter for Lambda terms; Starting with Monads + K - reduce_stage1 --> K - reduce_stage1 --> K + # #trace reduce_try1;; + reduce_try1 is now traced. + +The first `#` there is OCaml's prompt. The text beginning `#trace ...` is what we typed. Now OCaml will report on all the input to, and results from, the `reduce_try1` function. Watch: + + # reduce_try1 (App (I, App (I, K)));; + reduce_try1 <-- App (I, App (I, K)) + reduce_try1 <-- App (I, K) + reduce_try1 <-- K + reduce_try1 --> K + reduce_try1 --> K + reduce_try1 --> K - : term = K In the trace, "`<--`" shows the input argument to a call to -`reduce_stage1`, and "`-->`" shows the output result. +`reduce_try1`, and "`-->`" shows the output result. Since the initial input (`I(IK)`) is a redex, the result after the -one-step reduction is `IK`. We recursively call `reduce_stage1` on +one-step reduction is `IK`. We recursively call `reduce_try1` on this input. Since `IK` is itself a redex, the result after one-step -reduction is `K`. We recursively call `reduce_stage1` on this input. Since +reduction is `K`. We recursively call `reduce_try1` on this input. Since `K` is not a redex, the recursion bottoms out, and we return the result. @@ -193,24 +204,24 @@ the following reduction path: But the reduction function as written above does not deliver this result: - # reduce_stage1 (App (App (I, I), K));; + # reduce_try1 (App (App (I, I), K));; - : term = App (App (I, I), K) The reason is that the top-level term is not a redex to start with, -so `reduce_stage1` returns it without any evaluation. +so `reduce_try1` returns it without any evaluation. -What we want is to -evaluate the subparts of a complex term. We'll do this by evaluating -the subparts of the top-level expression. +What we want is to evaluate the subterms of a complex term. We'll do this by pattern matching our +top-level term to see when it _has_ subterms: - let rec reduce (t:term):term = match t with - I -> I + let rec reduce_try2 (t : term) : term = match t with + | I -> I | K -> K | S -> S | App (a, b) -> - let t' = App (reduce a, reduce b) in - if (is_redex t') then reduce 2 (reduce_one_step t') - else t' + let t' = App (reduce_try2 a, reduce_try2 b) in + if (is_redex t') then let t'' = reduce_if_redex t' + in reduce_try2 t'' + else t' Since we need access to the subterms, we do pattern matching on the input. If the input is simple (the first three `match` cases), we @@ -221,24 +232,24 @@ at the top level. To understand how this works, follow the trace carefully: - # reduce (App(App(I,I),K));; - reduce <-- App (App (I, I), K) + # reduce_try2 (App(App(I,I),K));; + reduce_try2 <-- App (App (I, I), K) - reduce <-- K ; first main recursive call - reduce --> K + reduce_try2 <-- K ; first main recursive call + reduce_try2 --> K - reduce <-- App (I, I) ; second main recursive call - reduce <-- I - reduce --> I - reduce <-- I - reduce --> I - reduce <-- I - reduce --> I - reduce --> I + reduce_try2 <-- App (I, I) ; second main recursive call + reduce_try2 <-- I + reduce_try2 --> I + reduce_try2 <-- I + reduce_try2 --> I + reduce_try2 <-- I + reduce_try2 --> I + reduce_try2 --> I - reduce <-- K ; third - reduce --> K - reduce --> K + reduce_try2 <-- K ; third + reduce_try2 --> K + reduce_try2 --> K - : term = K Ok, there's a lot going on here. Since the input is complex, the @@ -259,12 +270,12 @@ In any case, in the second main recursive call, we evaluate `II`. The result is `I`. At this point, we have constructed `t' == App(I,K)`. Since that's a -redex, we ship it off to reduce_one_step, getting the term `K` as a +redex, we ship it off to reduce_if_redex, getting the term `K` as a result. The third recursive call checks that there is no more reduction work to be done (there isn't), and that's our final result. You can see in more detail what is going on by tracing both reduce -and reduce_one_step, but that makes for some long traces. +and reduce_if_redex, but that makes for some long traces. So we've solved our first problem: `reduce` now recognizes that `IIK ~~> K`, as desired. @@ -273,7 +284,7 @@ Because the OCaml interpreter evaluates each subexpression in the course of building `t'`, however, it will always evaluate the right hand subexpression, whether it needs to or not. And sure enough, - # reduce (App(App(K,I),skomega));; + # reduce_try2 (App(App(K,I),skomega));; C-c C-cInterrupted. Running the evaluator with this input leads to an infinite loop, and @@ -297,25 +308,26 @@ type term = I | S | K | App of (term * term) data Term = I | S let skomega = App (App (App (S,I), I), App (App (S,I), I)) skomega = (App (App (App S I) I) (App (App S I) I)) - reduce_one_step :: Term -> Term -let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of - App(I,a) -> a App I a -> a + reduce_if_redex :: Term -> Term +let reduce_if_redex (t:term):term = match t with reduce_if_redex t = case t of + | App(I,a) -> a App I a -> a | App(App(K,a),b) -> a App (App K a) b -> a | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) App (App (App S a) b) c -> App (App a c) (App b c) | _ -> t _ -> t is_redex :: Term -> Bool -let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t) +let is_redex (t:term):bool = not (t = reduce_if_redex t) is_redex t = not (t == reduce_if_redex t) - reduce :: Term -> Term -let rec reduce (t:term):term = match t with reduce t = case t of - I -> I I -> I + reduce_try2 :: Term -> Term +let rec reduce_try2 (t : term) : term = match t with reduce_try2 t = case t of + | I -> I I -> I | K -> K K -> K | S -> S S -> S - | App (a, b) -> App a b -> - let t' = App (reduce a, reduce b) in let t' = App (reduce a) (reduce b) in - if (is_redex t') then reduce (reduce_one_step t') if (is_redex t') then reduce (reduce_one_step t') - else t' else t' + | App (a, b) -> App a b -> + let t' = App (reduce_try2 a, reduce_try2 b) in let t' = App (reduce_try2 a) (reduce_try2 b) in + if (is_redex t') then let t'' = reduce_if_redex t' if (is_redex t') then reduce_try2 (reduce_if_redex t') + in reduce_try2 t'' else t' + else t' There are some differences in the way types are made explicit, and in @@ -324,16 +336,16 @@ Haskell). But the two programs are essentially identical. Yet the Haskell program finds the normal form for `KIΩ`: - *Main> reduce (App (App K I) skomega) + *Main> reduce_try2 (App (App K I) skomega) I Woa! First of all, this is wierd. Haskell's evaluation strategy is called "lazy". Apparently, Haskell is so lazy that even after we've -asked it to construct t' by evaluating `reduce a` and `reduce b`, it -doesn't bother computing `reduce b`. Instead, it waits to see if we +asked it to construct `t'` by evaluating `reduce_try2 a` and `reduce_try2 b`, it +doesn't bother computing `reduce_try2 b`. Instead, it waits to see if we ever really need to use the result. -So the program as written does NOT fully determine evaluation order +So the program as written does _not_ fully determine evaluation order behavior. At this stage, we have defined an evaluation order that still depends on the evaluation order of the underlying interpreter. @@ -353,20 +365,19 @@ wait until we have Continuation Passing Style transforms. The answer to the first question (Can we adjust the OCaml evaluator to exhibit lazy behavior?) is quite simple: -
-let rec reduce_lazy (t:term):term = match t with
-    I -> I
-  | K -> K
-  | S -> S
-  | App (a, b) -> 
-      let t' = App (reduce_lazy a, b) in
-        if (is_redex t') then reduce_lazy (reduce_one_step t')
-                         else t'
-
- -There is only one small difference: instead of setting `t'` to `App -(reduce a, reduce b)`, we omit one of the recursive calls, and have -`App (reduce a, b)`. That is, we don't evaluate the right-hand + let rec reduce_lazy (t : term) : term = match t with + | I -> I + | K -> K + | S -> S + | App (a, b) -> + let t' = App (reduce_lazy a, b) in + if (is_redex t') then let t'' = reduce_if_redex t' + in reduce_lazy t'' + else t' + +There is only one small difference from `reduce_try2`: instead of setting `t'` to `App +(reduce_try3 a, reduce_try3 b)`, we omit one of the recursive calls, and have +`App (reduce_try3 a, b)`. That is, we don't evaluate the right-hand subexpression at all. Ever! The only way to get evaluated is to somehow get into functor position.