# Questions tagged [variable-binding]

The tag has no usage guidance.

40 questions
Filter by
Sorted by
Tagged with
12k views

### 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?
• 451
2k views

### Barendregt's Variable Convention: what does it mean?

Barendregt's Variable Convention: If $M_1,...,M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free ...
• 1,014
4k views

### What is the difference between assignment, valuation and name binding?

I read that Name binding assigns some value (data/code/expression) to an identifier. Assignment and valuation seem to do the same thing. It is confusing. Can I just tell that free variable is one, ...
• 837
630 views

### Free and bound variables

I am familiar with free and bound variables theory , but while learning I somewhere saw this lambda expression ((lambda var ((fn1 var) & (fn2 var))) argument) From what I have learned it ...
• 184
16k views

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

My teacher has provided the following pseudo-code, and says that the output using static scope is 1 2 3, but the output using dynamic scope is ...
1k views

### what is variable capture in nominal logic?

While reading a paper Nominal Unification from a Higher-Order Perspective, in the abstract I noticed something feel bit confusing, Nominal Logic is an extension of first-order logic with equality, ...
• 1,014
471 views

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

On page 7/8, section 1.2, of Practical Foundations of Programming Languages, 2nd edition, Robert Harper gives this initial definition of abstract binding trees: The smallest family of sets closed ...
• 307
361 views

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

The role of $x$ in $\frac{\mathrm{d}}{\mathrm{d}x} y$ not only confuses my calculus students, it has also puzzled some well known mathematicians. Questions one might ask are: Does the $x$ in the ...
3k views

### Static scope and dynamic scope

I am perpetually confused when it comes to static scoping and dynamic scoping and their differences and Wikipedia isn't of any help, so here's my question: Given the following pseudo code in a ...
152 views

• 131
102 views

### Lemma relating variable substitution to de Bruijn substitution

Notation: Let $t$ and $u$ be terms in the $\lambda$-calculus, and $x$ be a variable name. Let $[x\mapsto u]t$ be the substitution in $t$ of free variable $x$ for the term $u$. Specifically, I'm ...
94 views

### Semantics of "write-once" variables for complex data structures

Question My use case for what is described below is not a language or compiler implementation, but finding a reasonable semantics for this feature in a an abstract calculus. Ideally, you give me a ...
• 370
2k views

### How do global variables and automatic variables with the same name interact?

Suppose I define a global variable and I define an automatic variable within a function definition with the same name as the aforementioned global variable. What would happen to the global variable ...
33 views

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

I am currently reading the Crafting Interpreter book and I have a question about the Resolving and Binding chapter The author gave this example to illustrate the problem with the implementation at ...
• 145
81 views

• 129
37 views

### formal definition of lexical scope

I wonder if there is a formal definition of lexical scope so that people can prove things with respect to it, for example, that an interpreter implements lexical scope. You may ask what level of ...
• 781