33 votes
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 ...
Joey Eremondi's user avatar
24 votes

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 ...
user253751's user avatar
  • 1,739
8 votes

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 ...
Gilles 'SO- stop being evil''s user avatar
5 votes

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 ...
frabala's user avatar
  • 801
5 votes
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 ...
Andrej Bauer's user avatar
  • 30.4k
5 votes

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 ...
Draconis's user avatar
  • 7,138
4 votes

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 ...
chi's user avatar
  • 14.6k
4 votes
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'...
chi's user avatar
  • 14.6k
4 votes
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, ...
Alexey Romanov's user avatar
4 votes

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 ...
Amareswar Reddy's user avatar
4 votes
Accepted

What are differences between Static Scope and Dynamic Scope?

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 ...
Evil's user avatar
  • 9,455
4 votes
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 ...
Kurt Mueller's user avatar
3 votes
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 ...
Highheath's user avatar
  • 1,048
3 votes

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 ...
Jean Abou Samra's user avatar
2 votes

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 ...
Scott Cooper's user avatar
2 votes
Accepted

Claimed problems with Lisp dynamic scoping

With fact, the primary problem is with f. If n is 0, ...
Nathan Davis's user avatar
2 votes

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

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 $\...
Michael Bächtold's user avatar
2 votes

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 ...
gnasher729's user avatar
2 votes
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.
D.W.'s user avatar
  • 159k
2 votes
Accepted

Free variable in the programming language

Can we say only global variables are the free variables? No. Counterexample in ECMAScript: ...
Jörg W Mittag's user avatar
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 ...
user123's user avatar
  • 1,112
1 vote

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

I suspect you're imagining $\text{let } x = E \text{ in } E'$ as describing a sequence of steps: take the thing described by $E$ and put it in the box labeled $x$, then proceed to the thing labeled $E'...
benrg's user avatar
  • 2,112
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. ...
D.W.'s user avatar
  • 159k
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 ...
D.W.'s user avatar
  • 159k
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 ...
D.W.'s user avatar
  • 159k
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 ...
chi's user avatar
  • 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 ...
alim's user avatar
  • 994
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 ...
PMar's user avatar
  • 11

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