Question

I am specifically focusing on lambda calculus, following this paper: A Tutorial Introduction to the Lambda Calculus.

Suppose we have three functions that represent the natural numbers 0 and 1, and a successor function:

$\lambda sz.z = 0$

$\lambda sz.s(z) = 1$

$\lambda wyx.y(wyx) = succ$

Suppose I were to evaluate $succ\ succ\ 1$. As I evaluate this expression, it is becoming clear to me that it's not 3 as I might naively expect, but I do not truly grasp "why." Even as I go through the motions of evaluating the expression, I do not understand the nature of the turn of events and why certain expressions produce a certain result due to their structure and construction.

A question I might ask would be something like, why does $succ$ have that form, and is there an alternative form for $succ$ that produces the same result? If it is unique, what makes it special? I don't know how to answer these questions well yet, so I am seeking guidance.

Is there a method by which I can better visualize or understand the evaluation of expressions and how it affects the "class" of their output? I am very new to lambda calculus, so please excuse me.

Edit: I think I understand the rules for evaluation of lambda calculus (substitution, prevention of name collisions, etc.), but I have a hard time understanding the arbitrary rules by which one can construct lambda calculus' equivalent forms for the natural numbers, the successor functions, and the addition and multiplication functions. It's how these parallels to these concepts were mapped over to lambda calculus that I am interested in.

For example, why are the functions for "choose second," "false," and "discard next argument," and "0" have the same form and thus equivalent? There exists systems in which applying the zero function to a list of object does not result in returning a list with the front-most argument removed. Even if it is a convention, is there a reason why it is structured as such?

For example, why is does the successor function work? One can say that it was discovered through trial and error, but this makes for poor understanding of the nature of a concept besides "it is so" and "it works." I hope this makes sense.

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top