Iteration function in lambda calculus

Question

I have a function like this

iter :: Int -> (a -> a) -> a -> a    
iter n f a = f (f ... (f a) .. )

how can i define such function in un-typed lambda calculus ?

any hint/help will be appreciated.

you might get a better response at: cstheory.stackexchange.com — Dhaivat Pandya
– Dhaivat Pandya, Commented Apr 25, 2011 at 13:45
@Dhaivat: Sure, if you count "This question is for research-level questions only - please read the FAQ" as a better response. — sepp2k
– sepp2k, Commented Apr 25, 2011 at 14:06
Its not really research level, but, I doubt that one could find many people who work with lambda calculus on SO, seeing that it is a highly "work-based" community. — Dhaivat Pandya
– Dhaivat Pandya, Commented Apr 25, 2011 at 15:22
The question is bogus: what does ... mean? (I know what you think it means, but that's exactly where your problem is.) — Eli Barzilay
– Eli Barzilay, Commented Apr 25, 2011 at 18:06

gasche · Accepted Answer · 2011-04-26 05:57:45Z

1

Numbers do not exist per se in pure lambda calculus. You have to design a representation for numbers (and show that indeed those behave like numbers). The basic idea is that you can define numbers so that they are exactly the iteration function you need : n would be a lambda term that, when given a function f, compute the nth iteration of f.

This is an idea known as Church Encoding.

answered Apr 26, 2011 at 5:57

gasche

31.5k3 gold badges81 silver badges100 bronze badges

Sign up to request clarification or add additional context in comments.

1 Comment

dinsim Over a year ago

Thank you for your answer, you are absolutely right, i figured it out later, it would give the Church numerals representation in lambda calculus

René Höhle · Accepted Answer · 2013-10-04 12:01:25Z

0

iter == (rec g (fn f (fn n (fn x ((= n 0) x (g f (- n 1) (f x)))))))

edited Oct 4, 2013 at 12:01

René Höhle

27.4k22 gold badges78 silver badges91 bronze badges

answered Oct 4, 2013 at 11:42

Taoufik Dachraoui

411 bronze badge

2 Comments

Taoufik Dachraoui Over a year ago

I designed and implemented a lisp dialect that is strongly typed with implicit types where the iter function could be written as follows using y-comb:

(let ((p (fn u (fn v (v ((u u) v))))) 	(Y (p p)) 	(iter (Y (fn (lazy iter) 		    (fn (n f a) 			((eqw n 0) 			 a 			 (iter (subw n 1) f (f a))))))))     (iter 3 (fn x (mulw x x)) 2))

and also as: ((label iter (fn (n f a) ((eqw n 0) a (iter (subw n 1) f (f a))))) 3 (fn x (mulw x x)) 2)

Taoufik Dachraoui Over a year ago

using the iter function we can construct a cyclic structure as follows:

((label iter 	 (fn (n f a) 	     ((eqw n 0) 	      a 	      (iter (subw n 1) f (f a)))))     3 (fn x (set (cdr x) (cons x nil))) (cons nil nil))

Collectives™ on Stack Overflow

Iteration function in lambda calculus

2 Answers 2

1 Comment

2 Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

1 Comment

2 Comments

Your Answer

Sign up or log in

Post as a guest

Related