32

I'd suggest you look into the wonderful world of Compiler Construction! The answer is that it's a bit of a complicated process. To try to give you an intuition, remember that variable names are purely there for the programmer's sake. The computer will ultimately turn everything into addresses at the end. Local variables are (generally) stored on the stack: ...


24

When a computer stores a variable, when a program needs to get the variable's value, how does the computer know where to look in memory for that variable's value? The program tells it. Computers do not natively have a concept of "variables" - that's entirely a high-level language thing! Here's a C program: int main(void) { int a = 1; return a + 3; ...


9

In the usual mathematical notation: $(\lambda \color{blue}{x}. (\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))) A$ The two green occurrences of $\color{green}{x}$ in the subterms $f_1 \color{green}{x}$ and $f_2 \color{green}{x}$ are bound in the term $\lambda \color{blue}{x}. (\& (f_1 \color{green}{x}) (f_2 \color{green}{x}))$. The binding ...


7

Binding has to do with giving names to things (or values) in a given well delimited context. Assignment is about storing things (or values) in some location (a variable). Another assignment can replace a previous value with a new one. Valuation consist in binding all the identifiers of a formal text with something (with a value). In mathematics these ...


7

A subterm of a closed term is not necessarily a closed term. A calculus of closed terms would have to model open terms as well anyway. Pretty much any definition on terms relies on induction over the structure of the terms, and to define something for closed terms of the form $\lambda x. M$, you need to define that thing for the open term $M$. There are ...


5

The answer here is the same as in the other question: one thing is missing here! Your addition result should be: $$3 + 4 = \lambda g . \lambda z . 3 g (4 g z) = \lambda g . \lambda z . 7 g z$$ Note that $g$ is now a lambda parameter, not a free variable! So now if you want to apply this to something, it'll get substituted in the same everywhere: $$7 q r =...


5

In a nutshell There are two issues that justify the statement of your reference: The free or bound character of a variable depends on how much context you are considering, and whether it contains a binding occurrence of the variable A variable may be re-bound within the scope of an existing binding, so that removing that binding does not preclude that some ...


5

Variable capture is the phenomenon which "breaks" things when you do your substitutions in a naive way. For example: Correct: in the expression $$\int_0^1 (a + x)^2 dx$$ substitute $t^2$ for $a$, to get $$\int_0^1 (t^2 + x)^2 dx.$$ Correct: in the expression $$\int_0^1 (a + t)^2 dt$$ substitute $t^2$ for $a$, to get $$\int_0^1 (t^2 + u)^2 du$$ (we renamed ...


5

All three notions are related to variables. You can think of variables as named placeholders for some expression. When introducing/declaring a new variable, you create a placeholder for an abstract expression (abstract in the sense that the variable does not represent a particular expression). Every variable declaration creates also a scope for that ...


4

Some background, from https://www.youtube.com/watch?v=6m_RLTfS72c: What is static scope ? Static scope refers to scope of a variable is defined at compile time itself that is when the code is compiled a variable to bounded to some block scope if it is local, can be bounded to entire Main block if it is global. examples: C,C++, Java uses static scoping ...


4

In static scope the $fun2$ takes the globally scoped $c$ which comes from scope where function is defined (opposite to dynamic, where it traverses scopes of execution), so $c = 3$. With dynamic scope traverses up the chain of scopes until it finds variable it needs, which reflects the fact that scopes are: Global($a=1, b=2, c=3$) -> main($c=4$) -> fun1 ($a=2,...


4

Here is the simulation by hand. call by need using static scope The function receives as x parameter the thunk [n+m] bound to the globals. Then local n gets 10. The print statement requires evaluation of the thunk, which becomes 100+5, i.e. 105. It prints 105+10, i.e. 115. Local n and global m are changed, but this cannot affect x for two reasons: the ...


4

wrong in assuming that bound and free are full complements Yes. Each occurrence of a variable is either bound or free, but not both. But a variable is considered free if it has any free occurrences, and it's bound if it has any bound occurrences; it can be both at once.


3

Just to clear something up that may not have been obvious, $\chi$ is a set and the notation $B[\chi, x]$ is meant to be ABTs under free variables that are either $x$ or are in $\chi$. In this notation I believe it is implied that $x \notin \chi$ when you write $B[\chi, x]$, which is important. Using the definition of ABT above, you cannot prove for any $\...


3

Free variables never get $\alpha$-converted, only bound variables can. In the term $(\lambda x.\ xy)$ we can rename the bound variable $x$ to any other variable (except $y$, since that would cause a name clash). For instance, we can obtain $(\lambda z.\ zy)$. Instead, we can never rename $y$, since that is free, not being under any $\lambda y$. By contrast,...


3

The recursion combinator you mention seems to be the recursor associated to an inductive (or recursive) data type. In the paper this seems to be the type describing the syntax of lambda terms. Here, I'll take lists as a simpler recursive type. Note that the "lists of naturals type" can be intuitively described as the "least" type admitting these ...


3

As Raphael says in his comment, this is a hierarchical scope organization. But this can qualified any kind of tree structured scope, and you state in the title that it is tree structured. The whole purpose of this hierarchy is to allow reusing the same name in a different scope, for some other naming purpose. So, given a name, you have to decide where to ...


3

This seems to me (as to some commenters) to be simply dynamic scoping. It was used often in Lisp to change the behavior of system functions to get some extra features, or perform hidden actions such as monitoring of programs. The cost is indeed that large programs may be difficult to manage and maintain. Since then, there was a long battle between static ...


3

Not that I know of, but "stateful function" is reasonably descriptive. In informal conversation, that's what I'd use, as long as I suspect the audience will understand what I mean. In formal writing, I might still use the same phrase but also provide a careful definition of what I meant by that phrase. Really, that's a large part of what "formal" writing ...


3

In most programming languages, especially imperative languages, a “variable” is actually two things: a name and a storage location. The storage location is a block of memory where a value can be stored and retrieved. The variable's name is often called an identifier. An identifier is a way to refer to some object in the program, in this case a storage ...


2

This is a good question, though extremely elementary. I try to give you a very general answer. There are variations with different programming languages, or other types of languages. The issue is really about the role of names, that we usually call identifiers in programming. First note that a global variable may also be an automatic variable, but it is ...


2

Beta-reduction is only allowed when the argument does not contain any free variable that is bound in the function. So before you can beta-reduce $(\lambda x. \lambda y.x) y$, you must rename the bound variable $y$ using alpha-conversion. Formally speaking, beta-reduction and equivalence are defined not over lambda terms, but over lambda terms modulo alpha-...


2

When the compiler or interpreter encounters the declaration of a variable, it decides what address it will use to store that variable, and then records the address in a symbol table. When subsequent references to that variable are encountered, the address from the symbol table is substituted. The address recorded in the symbol table may be an offset from a ...


2

It depends on the programming language. It's up to each language to specify whether this is legal or not, and what it means. In many languages this would be legal. It is called variable shadowing.


2

With fact, the primary problem is with f. If n is 0, then it works fine. However, for any other value of n, fact is called with an f of () => n * f(). So when the base case (n = 0) is finally encountered, f is () => n * f(). When f is invoked, f is still () => n * f(). So the call to f results in unbounded recursion with itself. With ...


2

Some mathematicians find it natural to substitute for the variable in the denominator of a derivative, writing things like $\frac{d \log V}{d\log p}$. This suggests that the $x$ in the denominator $\frac{dy}{dx}$ is neither bound nor binding nor a symbol. Rather $\frac{dy}{dx}$ seems to be an operation on "variable quantities" $y,x$ requiring some side ...


2

It is in many languages legal to create a variable in an inner scope with the same name as a variable in an outer scope. The problem is that this may have been done by accident, and you never wanted to create a second variable, or that you use the inner variable when you wanted to use the outer one. For that reason, many compilers will issue a warning in ...


1

Yes. This appears to be an instance of the assignment problem. In the assignment problem, you construct a bipartite graph. The vertices on the left represent referees. The vertices on the right represent matches. You draw an edge from a referee $r$ to a match $m$ if the referee $r$ is potentially available to officiate in that match. You can use the ...


1

Functions of a single variable We can define a operator $\mathcal{D}$ on functions $f: \mathbb{R} \to \mathbb{R}$ so that $\mathcal{D}(f)$ is the first derivative of $f$. It is common to write this operator without parentheses, i.e., write it as $\mathcal{D} f$ instead of $\mathcal{D}(f)$ and write $\mathcal{D} f(x)$ instead of $(\mathcal{D}(f))(x)$ or $\...


1

Roughly put, every time you define a function, as in def B(): ... you define B to be a closure. This is a pair contains a representation of the body of the function (possibly compiled to a simpler language), and a reference to the current environment (possibly restricted to what B actually needs). The current environment is the one we are in when we run def ...


Only top voted, non community-wiki answers of a minimum length are eligible