projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
bcf5a36
)
tweaks
author
jim
<jim@web>
Sun, 22 Feb 2015 21:57:55 +0000
(16:57 -0500)
committer
Linux User
<ikiwiki@localhost.members.linode.com>
Sun, 22 Feb 2015 21:57:55 +0000
(16:57 -0500)
topics/week4_more_about_fixed_point_combinators.mdwn
patch
|
blob
|
history
diff --git
a/topics/week4_more_about_fixed_point_combinators.mdwn
b/topics/week4_more_about_fixed_point_combinators.mdwn
index
11754dd
..
763c18b
100644
(file)
--- a/
topics/week4_more_about_fixed_point_combinators.mdwn
+++ b/
topics/week4_more_about_fixed_point_combinators.mdwn
@@
-60,15
+60,15
@@
Used in a context in which *this sentence meaning* refers to the meaning express
or `\m y n. m n y`, which is the `C` combinator. So in such a
context, (2) might denote
or `\m y n. m n y`, which is the `C` combinator. So in such a
context, (2) might denote
- Y C
- (\h. (\u. h (u u)) (\u. h (u u))) C
- (\u. C (u u)) (\u. C (u u)))
- C ((\u. C (u u)) (\u. C (u u)))
- C (C ((\u. C (u u)) (\u. C (u u))))
- C (C (C ((\u. C (u u)) (\u. C (u u)))))
+ Y C
≡
+ (\h. (\u. h (u u)) (\u. h (u u))) C
~~>
+ (\u. C (u u)) (\u. C (u u)))
~~>
+ C ((\u. C (u u)) (\u. C (u u)))
~~>
+ C (C ((\u. C (u u)) (\u. C (u u))))
~~>
+ C (C (C ((\u. C (u u)) (\u. C (u u)))))
~~>
...
...
-An
d
infinite sequence of `C`s, each one negating the remainder of the
+An infinite sequence of `C`s, each one negating the remainder of the
sequence. Yep, that feels like a reasonable representation of the
liar paradox.
sequence. Yep, that feels like a reasonable representation of the
liar paradox.
@@
-161,13
+161,13
@@
of `N`, by the reasoning in the previous answer.
A: Right:
A: Right:
- let Y = \
N. (\u. N (u u)) (\u. N
(u u)) in
- Y Y
- ≡ \N. (\u. N (u u)) (\u. N (u u)) Y
- ~~> (\u. Y (u u)) (\u. Y (u u))
- ~~> Y ((\u. Y (u u)) (\u. Y (u u)))
- ~~> Y ( Y ((\u. Y (u u)) (\u. Y (u u))))
-
~~> Y (Y (
Y (...(Y (Y Y))...)))
+ let Y = \
h. (\u. h (u u)) (\u. h
(u u)) in
+ Y Y
≡
+ \h. (\u. h (u u)) (\u. h (u u)) Y ~~>
+ (\u. Y (u u)) (\u. Y (u u)) ~~>
+ Y ((\u. Y (u u)) (\u. Y (u u))) ~~>
+ Y ( Y ((\u. Y (u u)) (\u. Y (u u)))) <~~>
+
Y ( Y (
Y (...(Y (Y Y))...)))
@@
-176,8
+176,8
@@
A: Right:
A: Is that a question?
Let's come at it from the direction of arithmetic. Recall that we
A: Is that a question?
Let's come at it from the direction of arithmetic. Recall that we
-claimed that even `succ`
---
the function that added one to any
-number
---
had a fixed point. How could there be an `ξ` such that `ξ <~~> succ ξ`?
+claimed that even `succ`
---
the function that added one to any
+number
---
had a fixed point. How could there be an `ξ` such that `ξ <~~> succ ξ`?
That would imply that
ξ <~~> succ ξ <~~> succ (succ ξ) <~~> succ (succ (succ ξ)) <~~> succ (...(succ ξ)...)
That would imply that
ξ <~~> succ ξ <~~> succ (succ ξ) <~~> succ (succ (succ ξ)) <~~> succ (...(succ ξ)...)
@@
-294,19
+294,19
@@
So for instance:
`A 1 x` is to `A 0 x` as addition is to the successor function;
`A 2 x` is to `A 1 x` as multiplication is to addition;
`A 1 x` is to `A 0 x` as addition is to the successor function;
`A 2 x` is to `A 1 x` as multiplication is to addition;
-`A 3 x` is to `A 2 x` as exponentiation is to multiplication---
+`A 3 x` is to `A 2 x` as exponentiation is to multiplication
---
so `A 4 x` is to `A 3 x` as hyper-exponentiation is to exponentiation...
## Q: What other questions should I be asking? ##
so `A 4 x` is to `A 3 x` as hyper-exponentiation is to exponentiation...
## Q: What other questions should I be asking? ##
-* What is it about the variant fixed-point combinators that makes
- them compatible with a call-by-value evaluation strategy?
+* What is it about the "primed" fixed-point combinators `Θ′` and `Y′` that
+ makes them compatible with a call-by-value evaluation strategy?
+
+* What *exactly* is primitive recursion?
* How do you know that the Ackermann function can't be computed
using primitive recursion techniques?
* How do you know that the Ackermann function can't be computed
using primitive recursion techniques?
-* What *exactly* is primitive recursion?
-
* I hear that `Y` delivers the/a *least* fixed point. Least
according to what ordering? How do you know it's least?
Is leastness important?
* I hear that `Y` delivers the/a *least* fixed point. Least
according to what ordering? How do you know it's least?
Is leastness important?