# Tag Info

Accepted

### Lambda Calculus in Rewriting systems

See also this question: "How is Lambda Calculus a specific type of Term Writing system?". Term rewriting, as introduced in (1), and described in e.g. (2), is a first-order system that cannot handle ...
• 8,328
Accepted

### Intuitive explanation of neutral / normal form in lambda calculus

I can reassure you that this property is not immediately self-evident. In trying to describe/enumerate the set of normal forms, the main observation required is the following: Abstraction preserves ...
• 8,233
Accepted

### Confluence of beta expansion

Two counterexamples are: $(\lambda x. b x (b c)) c$ and $(\lambda x. x x) (b c)$ (Plotkin). $(\lambda x. a (b x)) (c d)$ and $a ((\lambda y. b (c y)) d)$ (Van Oostrom). The counterexample detailed ...
Accepted

### call by value: what is a value?

The set of values is defined for a particular reduction relation. Each reduction relation defines its own set of values. Reduction for the lambda calculus isn't just beta reduction, there are also ...

### What is congruence in lambda-calculus

Generally speaking, in algebra, a congruence relation is an equivalence relation such that operations on equivalent objects yield equivalent objects. In the lambda calculus, a congruence is an ...
Accepted

Accepted

### Semi-Thue system, which terminates

Consider the potential function $$\Phi(w_1 \ldots w_n) = \sum_{i=2}^n 2^i 1_{w_i = w_{i-1}}.$$ Applying one of the rewrite rules always decreases the potential: if we change $abb$ to $bab$ at ...
• 278k
Accepted

• 950
Accepted

First, let us show that the two assumptions are necessary. Here is an example showing what goes wrong when $x = y$. Take $t = x$, $u = 1$, $v = 2$. We have $$x\{x := 1\}\{x := 2\} = 1\{x := 2\} = 1, ... • 278k 3 votes ### Is there any count-preserving cellular automata which tends do "10101010..."? Seems like the rule: 000 => 000 001 => 100 010 => 010 100 => 100 011 => 011 101 => 101 110 => 101 111 => 111 Does what I want. Testing ... • 4,137 3 votes Accepted ### What does \text{dom}(\Gamma) mean in the context of an inference rule? There are various ways to define contexts in type theories. In this style, we assume there is some infinite set of variable names V and define the context \Gamma : V \rightharpoonup S as a partial ... • 661 3 votes ### Higher order rewriting theory and critical pairs with the beta rule The theory of higher-order critical pairs can indeed handle this example, as outlined in the following article: Higher-Order Rewrite Systems and their Confluence, Richard Mayr & Tobias Nipkow ... • 8,233 3 votes Accepted ### Is there a generic algorithm for translating equational rules into corresponding data structures? It sounds like what you are asking for is, for a given equational system \cal E, to give a canonical representation for equivalence classes modulo \cal E. Indeed, if your signature is the binary ... • 8,233 3 votes ### Term rewrite system for terms of lambda calculus? It's hard to understand what you are looking for, but perhaps you are looking for program transformations. A famous one is the CPS transform (continuation-passing style), which transforms any lambda ... • 14.6k 3 votes Accepted ### Properties of a term rewrite rule In general, there is no obstacle to define a rewrite system as above, and a few sources do indeed require rules 1. and 2. only as additional hypotheses. However the hypotheses are almost always ... • 8,233 3 votes ### When are you supposed to eta-reduce? \eta conversion is not a mean to reduce a term to \beta-normal form, but a tool to show equivalence regarding the (future) application; to express that 2 terms “are the same function”; that they ... • 1,191 2 votes Accepted ### Identifying/equating constants in a term rewrite system Counterexample: f(c) \rightarrow f(d) In general, there are some modularity theorems for termination and confluence that may apply if, e.g. your constants do not appear at all in any rule. There ... • 8,233 2 votes ### In what cases is graph rewriting not enough to avoid duplicate work? Consider this program: f (m : Nat) x y = (x, if H(m,m) then x else y) my_f = f my_number my_f hard harder where H(x,x) ... • 72.6k 2 votes ### What is the difference between deterministic and confluent? In terms of abstract rewriting, confluence and determinism are different notions. Let \to be a binary relation on a set. The relation \to is deterministic if b = c whenever b \leftarrow a \to c... • 21 2 votes Accepted ### What is the difference between deterministic and confluent? If a binary relation is confluent and terminating, then the map from initial state to final state is total and deterministic. The converse also holds. If a binary relation is confluent, the binary ... • 162k 2 votes Accepted ### Term-rewriting software recommendation PLT Redex has support for term rewriting. You'll find that most of the examples are focused on small-step operational semantics for programming languages, but in general the system allows for ... • 29.8k 2 votes Accepted ### Is there an algorithm for reducing CNFs further? CNF minimization is hard; see https://cstheory.stackexchange.com/q/9839/5038. It is certainly NP-hard, and there is a sense in which it is "even harder". One way to get some intuition why ... • 162k 2 votes Accepted ### Injectivity not required for unification algorithms? Here f is not a mathematical function. Rather, it is a function symbol. Don't think of f(a,b) as the result of evaluating the function at parameters a,b. Rather, think of it as a term in a ... • 162k 2 votes Accepted ### What is congruence in lambda-calculus "Congruence" in the context of lambda calculus is usually "alpha-congruence". "alpha-congruent" means "differring only if at all in the names of bound variables"... 2 votes Accepted ### Coding max as an interaction net Rules for agents in interaction nets are defined by what the principal port of that agent is connected to and each agent has exactly one principal port. In the "max" example, for the top ... • 56 2 votes Accepted ### A Markov algorithm that does unary multiplication You have demonstrated that example on multiplication cannot be correct. Well, there is typo in that example. The substitution rule p_3 should have been$$A\to\epsilon
• 39.1k
I don't know what is the definition for a reduction to be decidable. I would expect it is one of the following two: Defn 1: $\to$ is decidable iff there is an algorithm $A$ that always halts and, on ...