/prog/ - the lambda

Name: Anonymous 2013-02-21 1:16

We can define a successor function, which takes a number n and returns n + 1 by adding an additional application of f:

    SUCC := λn.λf.λx.f (n f x)

Because the m-th composition of f composed with the n-th composition of f gives the m+n-th composition of f, addition can be defined as follows:

    PLUS := λm.λn.λf.λx.m f (n f x)

PLUS can be thought of as a function taking two natural numbers as arguments and returning a natural number; it can be verified that

    PLUS 2 3

and

    5

are equivalent lambda expressions. Since adding m to a number n can be accomplished by adding 1 m times, an equivalent definition is:

    PLUS := λm.λn.m SUCC n

Name: Anonymous 2013-02-21 1:42

sounds rather complicated for 2 + 3 = 5

Name: Anonymous 2013-02-21 5:15

Yup, well done. The lambda calculus is indeed Turing-complete. What's your point though?

Name: Anonymous 2013-02-21 5:44

Now try to do this in the simply typed lambda calculus.

Name: Anonymous 2013-02-21 9:18

shouldn't you only need one lambda (-anonymous function) ?
plus = @(x,y) x+y;
plus(2,3)
ans = 5

Name: Anonymous 2013-02-21 11:25

>>5
Uh, are you fucking retarded? You forgot your ^^, by the way.

Name: Anonymous 2013-02-21 13:45

>>5
Define 2, define 3, define 5.

Name: Anonymous 2013-02-21 14:00

>>5
MATLAB-fag detected. Die in a fire, come back when you'll use a true programming langage.

Name: Anonymous 2013-02-21 15:11

>>8
Retard-kun likes MATLAB and Octave. Don't blame him, he doesn't even know about Church numerals.

Name: Anonymous 2013-02-21 15:15

>>5
Please don't open that cocksucking mouth of yours if you aren't going to contribute.

Name: Anonymous 2013-02-21 15:23

Finding λ is much like solving for an integer that should never exist in the first place. Its forced mathematical theory creating numbers from thin air. Solving for λ in statistics can be very funny at times. We have all heard from trolls, however much statistical analysis is trolling at its very best.

Name: Anonymous 2013-02-21 15:24

>>11
Another retard pretending to be a troll?

Name: Anonymous 2013-02-21 15:39

>>10
I was just about to suck your cock, faggot.

Name: Anonymous 2013-02-21 16:41

Wow, Presburger arithmetic. Why do I care?

Name: Anonymous 2013-02-21 16:42

>>14
Maybe Peano was a kike? I don't know.

Name: Anonymous 2013-02-21 17:59

XDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDD

Name: >>5 2013-02-21 18:29

What a bunch of whingers..
I'm sure next you'll tell me doing 1000000 ^ 2 by adding +1 at a time is optimal due to tail-call optimisations..

Name: Anonymous 2013-02-21 18:38

...I'm beginning to think Lisp probably isn't that slow at all..
Just that retards are using recursion for the sake of using recursion..

Name: Anonymous 2013-02-21 18:40

>>17
Who the fuck said this was about optimal implementations? This is purely a theoretical exercise. But no, you have to try to look smart, and then you make look yourself like a fucking idiot.

Fuck off back to /b/, gigantic dumbfuck.

Name: Anonymous 2013-02-21 18:46

>>19 o-kay.. So what theory should i have gleaned from this?

Name: Anonymous 2013-02-21 18:52

forgive me if i don't understand SUCC := λn.λf.λx.f (n f x)

Name: Anonymous 2013-02-21 18:54

where is the +1, and why are there three(?) variables for an increment function?

Name: Anonymous 2013-02-21 19:03

>>21
Church notation.
Zero: λf.λz.z = zero applications of f to z = z
One = succ(zero) = (λn.λf.λx.f (n f x))(λf.λz.z) = ... = f(z)
Two = succ(one) = f(f(z)) and so on.
I'm sure you can do the derivation, it's just substitution.

Name: Anonymous 2013-02-21 19:07

...you're using a succ function to implement a plus function.. if succ does anything other than just +1, it is a plus function. therefore plus is a recursive function.

why is plus a recursive function?

Name: Anonymous 2013-02-21 19:13

>>24
Your reasoning does not follow, does "recursive function" mean what you think it means?

Name: Anonymous 2013-02-21 19:17

>>26 perhaps not..
still 10 +10 seems to get broken into 10 +1 +1 +1 +1 +1 +1 +1 +1 +1 +1 ?

Name: Anonymous 2013-02-21 19:20

>>26
Yes, but also the first 10 gets broken down to 0 +1 +1 +1 +1 +1 +1 +1 +1 +1 +1.

Name: Anonymous 2013-02-21 19:22

>>27 it's worse than i thought?

Name: Anonymous 2013-02-21 19:28

why are you pulling numbers to pieces?

Name: Anonymous 2013-02-21 19:35

...so 1000000 + 1000000 results in 2000000 inlined succ calls?

Name: Anonymous 2013-02-21 19:46

>>30
What's interesting is that if you have another implementation that agrees with this one, you can prove things with either or and they apply to both.

Name: Anonymous 2013-02-21 19:53

>>20
Read SICP.

Name: Anonymous 2013-02-21 19:57

>>32 nigga please

Name: Anonymous 2013-02-21 20:00

>>5,17,20-22
What the fuck are you doing on my /prog/?

Name: Anonymous 2013-02-21 20:04

>>34 http://dis.4chan.org/read/music/1360783549/9

Name: Anonymous 2013-02-21 20:12

>>31 like optimality?

Name: Anonymous 2013-02-21 20:13

>>35
What? What does that have to do with my question? Why the fuck did you post that? Are you a spammer?

Name: Anonymous 2013-02-21 20:22

>>37 is your name elmo by any chance?

Name: Anonymous 2013-02-21 20:33

>>1
how do define substract?

Name: Anonymous 2013-02-21 20:34

>>38
No, you shithead.

Why do you try so hard to act ``funny''? Are you underage? And it's about time you answer my questions.

the lambda

1 Name: Anonymous 2013-02-21 1:16

2 Name: Anonymous 2013-02-21 1:42

3 Name: Anonymous 2013-02-21 5:15

4 Name: Anonymous 2013-02-21 5:44

5 Name: Anonymous 2013-02-21 9:18

6 Name: Anonymous 2013-02-21 11:25

7 Name: Anonymous 2013-02-21 13:45

8 Name: Anonymous 2013-02-21 14:00

9 Name: Anonymous 2013-02-21 15:11

10 Name: Anonymous 2013-02-21 15:15

11 Name: Anonymous 2013-02-21 15:23

12 Name: Anonymous 2013-02-21 15:24

13 Name: Anonymous 2013-02-21 15:39

14 Name: Anonymous 2013-02-21 16:41

15 Name: Anonymous 2013-02-21 16:42

16 Name: Anonymous 2013-02-21 17:59

17 Name: >>5 2013-02-21 18:29

18 Name: Anonymous 2013-02-21 18:38

19 Name: Anonymous 2013-02-21 18:40

20 Name: Anonymous 2013-02-21 18:46

21 Name: Anonymous 2013-02-21 18:52

22 Name: Anonymous 2013-02-21 18:54

23 Name: Anonymous 2013-02-21 19:03

24 Name: Anonymous 2013-02-21 19:07

25 Name: Anonymous 2013-02-21 19:13

26 Name: Anonymous 2013-02-21 19:17

27 Name: Anonymous 2013-02-21 19:20

28 Name: Anonymous 2013-02-21 19:22

29 Name: Anonymous 2013-02-21 19:28

30 Name: Anonymous 2013-02-21 19:35

31 Name: Anonymous 2013-02-21 19:46

32 Name: Anonymous 2013-02-21 19:53

33 Name: Anonymous 2013-02-21 19:57

34 Name: Anonymous 2013-02-21 20:00

35 Name: Anonymous 2013-02-21 20:04

36 Name: Anonymous 2013-02-21 20:12

37 Name: Anonymous 2013-02-21 20:13

38 Name: Anonymous 2013-02-21 20:22

39 Name: Anonymous 2013-02-21 20:33

40 Name: Anonymous 2013-02-21 20:34