# Tag Info

## Hot answers tagged variable-binding

Accepted

### How do computers remember where they store things?

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 ...
• 29.8k

### How do computers remember where they store things?

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 ...

### What benefits are obtained by allowing the occurrence of free variables and open terms in lambda calculus?

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 ...

### Is there a systematic way to know when to alpha-transform free variables?

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 ...
• 7,148
Accepted

### what is variable capture in nominal logic?

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 ...
• 30.9k

### Difference between assignment, binding, and substitution?

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 ...
• 801
Accepted

### what are Structural recursion, primitive recursion, recursion combinator and recursion principles?

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'...
• 14.6k
Accepted

### When is a variable bound or free in a lambda application?

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, ...
• 3,192

### What are differences between Static Scope and Dynamic Scope?

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 ...
Accepted

### How do I interpret the wording of this passage about abstract binding trees from the book Practical Foundations of Programming Languages

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 ...
• 743

### Is there a systematic way to know when to alpha-transform free variables?

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 ...
• 14.6k
Accepted

### How are closures supposed to interact with variable binding and resolving?

The scope of variables created with the var keyword in JS is pretty unintuitive, at least if you're already familiar with how other languages handle scope. You can ...
• 1,095

### What is a simple explanation and example of de Bruijn indices?

I suppose I do not understand why the definition needs multiple lambda terms M, N, …. Wouldn’t you just use de Bruijn indices for a single lambda term, such as lambda x . x + x? This is merely a ...

### How do computers remember where they store things?

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 ...

### Does hiding variables work in terms of blocks or line-by-line?

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 ...
• 30.6k
Accepted

### Does hiding variables work in terms of blocks or line-by-line?

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.
• 162k
Accepted

### Claimed problems with Lisp dynamic scoping

With fact, the primary problem is with f. If n is 0, ...
• 632

• 2,157
1 vote

### (how) is assignment or binding possible in purely functional languages?

The lambda calculus has names for the parameter (bound variable) to a lambda abstraction. That is the only mechanism or introducing names. Apart from that, there are no names in the lambda calculus. ...
• 162k
1 vote
Accepted

### What attributes are bound statically vs dynamically

I'm not an expert of C/linkers/binding but I'm not sure to understand what you mean with the code you provided. Static binding versus dynamic binding is very different and it has nothing to do with ...
• 1,112
1 vote
Accepted

### Relating indexes for parameters and variables

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 ...
• 162k
1 vote

### Is the $x$ in $\frac{\mathrm{d}}{\mathrm{d}x}$ a symbol in the sense of Harper's PFPL?

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 ...
• 162k
1 vote

### How shall I resolve a nonlocal name in a language with deep binding?

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 ...
• 14.6k
1 vote

### what is variable capture in nominal logic?

I find out it. in the higher-order unification, some function is found for variable $X$ such as $[X \mapsto \lambda y.y ]$, substituting this for $X$ will not lead to variable capture. in nominal ...
• 1,014
1 vote

### What are differences between Static Scope and Dynamic Scope?

POINT OF CLARIFICATION: The 'c' referred to in main() IS NOT DECLARED IN main(). Therefore there is only one 'c' in the program, the global one. When the program is run, this 'c' is first ...
• 11

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