Talk:Iota and Jot

Split

Maybe we should split this article. --Gp75motorsports (talk) 14:41, 11 December 2007 (UTC)

Exemples

This articles would be more complete with some examples to illustrate theses languages —Preceding unsigned comment added by 213.189.166.156 (talk) 11:32, 15 August 2008 (UTC)

Content is wrong

I think the statement made is not quite korrect: S ≠ U (U (U U)) = K

Assume

 S := λf g x. f x (g x)
 K := λx y. x
 U := λf. f S K

then

   U (U (U U))
 →    lookup U
   (λf. f S K) (U (U U))
 →    β-reduction
   U (U U) S K
 →    lookup U
   (λf. f S K) (U U) S K
 →    β-reduction
   U U S K S K
 →    lookup U
   (λf. f S K) U S K S K
 →    β-reduction
   U S K S K S K
 →    lookup U
   (λf. f S K) S K S K S K
 →    β-reduction
   S S K K S K S K
 →    lookup S
   (λf g x. f x (g x)) S K K S K S K
 →    β-reduction
   (λg x. S x (g x)) K K S K S K
 →    β-reduction
   (λx. S x (K x)) K S K S K
 →    β-reduction
   S K (K K) S K S K
 →    lookup S
   (λf g x. f x (g x)) K (K K) S K S K
 →    β-reduction
   (λg x. K x (g x)) (K K) S K S K
 →    β-reduction
   (λx. K x (K K x)) S K S K
 →    β-reduction
   K S (K K S) K S K
 →    lookup K
   (λx y. x) S (K K S) K S K
 →    β-reduction
   (λy. S) (K K S) K S K
 →    β-reduction
   S K S K
 →    lookup S
   (λf g x. f x (g x)) K S K
 →    β-reduction
   (λg x. K x (g x)) S K
 →    β-reduction
   (λx. K x (S x)) K
 →    β-reduction
   K K (S K)
 →    lookup K
   (λx y. x) K (S K)
 →    β-reduction
   (λy. K) (S K)
 →    β-reduction
   K  —Preceding unsigned comment added by 95.113.2.125 (talk) 10:58, 4 June 2010 (UTC)