1

I am extremely confused about this one.

  • Given the following rule ("Type and Programming Languages", Benjamin Pierce, page 72):
(λx.t)v2 -> [x -> v2]t (* E-AppAbs*)

Later in the same book, at page 87, we have (I simplified):

let is_value (e : expr) =
  match e with
  | Abstr (_, _)->true
  | _ -> false

let rec step e =
  match e with
  | App(Abstr(x, t1), v2) when is_value v2 -> subst x v2 t1 (*E-AppAbs*)
  | App(e1, e2) when is_value e1 -> App (e1, step e2) (*E-App2*)
  | App(e1, e2) -> App(step e1, e2) (*E-App1*)
  | _ -> raise NoRuleApplies

Note that is_value v2 is a necessary precondition before calling subst. I hence, conclude that the term (λx.x)y Is not reducible, because y is not a an abstraction.

  • However, I keep seeing this: enter image description here

(this is a screenshot from a Chicago university pdf, page 4)

Similarly, here, we can see that the accepted answers does:

(λx.xy)z   ->*   zy

This comes as contradiction to me, because, again, z above is not an abstraction.

Question: I don't understand what I am missing in definition, and why everyone keeps reducing stuff?

dgan
  • 1,349
  • 1
  • 15
  • 28
  • 1
    `(λx.x)y` would reduce in one "step" to `(λx.x) (step y)`, the evaluation of which will raise an exception. – molbdnilo Mar 26 '22 at 16:09
  • @molbdnilo yes, that's how I see it. However, that doesn't seem to be the case for examples I encounter on internet & in the book – dgan Mar 26 '22 at 16:23
  • I guess I would conclude that Pierce is using different definitions at this point from these other examples. FWIW I tried Pierce's code and indeed it doesn't seem to reduce either of the two examples you give. (The exception just causes evaluation to stop, it's not an error per se.) – Jeffrey Scofield Mar 26 '22 at 18:26
  • I’m voting to close this question because this question is off-topic on Stack Overflow and belongs instead on https://cs.stackexchange.com/. SO is for practical programming problems, not theoretical questions. See [help/on-topic]. (OCaml happens to have a high degree of academics in its programming community, so it isn't unlikely that you will receive a good answer here, but I still think you're much more likely to get a good answer on CS) – glennsl Mar 27 '22 at 09:03
  • it seems you need to add a clause to `is_value` to also admit naked variables as values, to make it work. something like `match e with | Abstr (_, _)->true | App(_,_) -> false | _ -> true` – Will Ness Mar 19 '23 at 01:53

0 Answers0