2. Throughout this problem, assume that we have
- let rec omega x = omega x;;
+ let rec blackhole x = blackhole x;;
All of the following are well-typed.
Which ones terminate? What are the generalizations?
- omega;;
+ blackhole;;
- omega ();;
+ blackhole ();;
- fun () -> omega ();;
+ fun () -> blackhole ();;
- (fun () -> omega ()) ();;
+ (fun () -> blackhole ()) ();;
- if true then omega else omega;;
+ if true then blackhole else blackhole;;
- if false then omega else omega;;
+ if false then blackhole else blackhole;;
- if true then omega else omega ();;
+ if true then blackhole else blackhole ();;
- if false then omega else omega ();;
+ if false then blackhole else blackhole ();;
- if true then omega () else omega;;
+ if true then blackhole () else blackhole;;
- if false then omega () else omega;;
+ if false then blackhole () else blackhole;;
- if true then omega () else omega ();;
+ if true then blackhole () else blackhole ();;
- if false then omega () else omega ();;
+ if false then blackhole () else blackhole ();;
- let _ = omega in 2;;
+ let _ = blackhole in 2;;
- let _ = omega () in 2;;
+ let _ = blackhole () in 2;;
3. This problem is to begin thinking about controlling order of evaluation.
The following expression is an attempt to make explicit the
However,
- let rec omega x = omega x in
- if true then omega else omega ();;
+ let rec blackhole x = blackhole x in
+ if true then blackhole else blackhole ();;
terminates, but
- let rec omega x = omega x in
+ let rec blackhole x = blackhole x in
let b = true in
- let y = omega in
- let n = omega () in
+ let y = blackhole in
+ let n = blackhole () in
match b with true -> y | false -> n;;
does not terminate. Incidentally, `match bool with true -> yes |