In Lambda Calculus, a **bound variable** is a variable whose scope is limited to a specific part of a lambda expression. It's essentially a placeholder that only has meaning within the context of that specific expression. Understanding bound variables is crucial for comprehending how lambda expressions work and how they represent functions. Here are some key points about bound variables: - **Defined within a lambda abstraction:** A bound variable is introduced within the body of a lambda abstraction using the lambda symbol (λ). For example, in the expression `λx. x + y`, `x` is a bound variable. - **Limited scope:** The scope of a bound variable is limited to the lambda abstraction that defines it. This means it can only be referenced within the body of that specific expression. - **Not accessible from outside:** Bound variables are not accessible from outside their scope. Trying to use them outside their lambda abstraction will result in an error. - **Alpha-conversion:** Bound variables can be renamed within their scope without affecting the meaning of the expression. This is called alpha-conversion and is crucial for maintaining syntactic consistency within lambda calculus. - **Contrast with free variables:** Bound variables are distinguished from free variables, which are not defined within a lambda abstraction and can be accessed from anywhere within the expression. Understanding bound variables is important because they play a fundamental role in defining and applying functions in lambda calculus. They allow for abstraction, where we can create generic functions that can be applied to different arguments. Here are some examples to illustrate the concept of bound variables: - **Simple bound variable:** ``` λx. x + 1 // Here, x is a bound variable ``` - **Multiple bound variables:** ``` λx. y + x // Here, both x and y are bound variables ``` - **Alpha-conversion:** ``` λx. x + y // original expression λz. z + y // renamed expression (x renamed to z) ``` # ChatGPT's Answer In lambda calculus, a bound variable is a variable that is defined within the scope of a lambda abstraction. It is called "bound" because its scope is limited to the expression in which it is defined. A bound variable represents an arbitrary value that can be substituted with other expressions in the lambda calculus notation. It contrasts with free variables, which are variables that are not bound by any lambda abstraction and can take on values from outside the current expression. ## How does a bound variable compare against a free variable A bound variable and a [[free variable]] are two different types of variables used in mathematical logic and formal systems. A bound variable is a variable that is defined within the scope of a quantifier. It is usually associated with a specific quantifier, such as the universal quantifier (∀) or the existential quantifier (∃). The scope of a bound variable is limited to the statement or formula in which it is defined. For example, in the statement "For all x, if P(x) then Q(x)", the variable x is a bound variable because it is defined within the scope of the universal quantifier "For all x". On the other hand, a free variable is a variable that is not bound by any quantifier and can take on any value. It is not restricted to any specific scope and can be used throughout an entire formula or system. For example, in the statement "P(x) implies Q(y)", both x and y are free variables because they are not bound by any quantifier. In terms of comparison, a bound variable and a free variable have different roles and behaviors within a logical system. A bound variable represents a specific object or element within its limited scope, while a free variable represents an arbitrary object that can be replaced by any value. Bound variables are often used to express general statements about all objects within their scope, while free variables allow for more flexibility in expressing statements about specific objects or conditions. It's important to note that the distinction between bound variables and free variables may vary depending on the context or formal system being used. In some cases, variables may be implicitly assumed to be either bound or free based on their usage within formulas or statements. # References ```dataview Table title as Title, authors as Authors where contains(subject, "bound variable") or contains(subject, "namespace") ```