Skip to main content
9 votes
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 ...
Martin Berger's user avatar
8 votes
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 ...
cody's user avatar
  • 8,233
8 votes
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 ...
Gilles 'SO- stop being evil''s user avatar
7 votes
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 ...
Gilles 'SO- stop being evil''s user avatar
6 votes

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

Confluence to show equivalent terms have one common reduct

$S \leftrightarrow^* T$ does not mean that $S \rightarrow^* T$ and $T \rightarrow^* S$! It means that there is a chain of reductions $S = S_0 \rightleftharpoons_1 S_1 \rightleftharpoons_2 S_2 \...
Gilles 'SO- stop being evil''s user avatar
4 votes
Accepted

When are you supposed to eta-reduce?

Here are some crucial properties about $\beta$ and $\eta$ reductions that explain the strategies for computing normal forms. We write $\rightarrow_\beta, \rightarrow_\eta$ for a single step of $\beta$...
cody's user avatar
  • 8,233
4 votes
Accepted

Term rewrite system for terms of lambda calculus?

I think that what you are looking for is called higher-order rewriting. There are systems in which you can define rewrite rules of the form $F\;(\lambda x.\lambda y.C\;X[x,y]) \longrightarrow X[X[t,u],...
Rodolphe Lepigre's user avatar
4 votes
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 ...
Yuval Filmus's user avatar
4 votes
Accepted

Understanding a boolean expression in λ-calculus

It's a very bad idea to omit parentheses. Correct is: $$\lambda b . b (\lambda x y . y) (\lambda x y . x)$$ Next, it is confusing to reuse bound variables, so let me rename them: $$\lambda b . b (\...
Andrej Bauer's user avatar
  • 30.9k
4 votes
Accepted

How was Idris' `rewrite` implemented?

I talked to be5invis and he said it's implemented using replace. replace is something like this in Agda: $$ replace : \forall \{...
ice1000's user avatar
  • 950
4 votes
Accepted

Proving equivalence of two substitutions by induction

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, $...
Yuval Filmus's user avatar
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 ...
MaiaVictor's user avatar
  • 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 ...
varkor's user avatar
  • 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 ...
cody's user avatar
  • 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 ...
cody's user avatar
  • 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 ...
chi's user avatar
  • 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 ...
cody's user avatar
  • 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 ...
Sandro Lovnički's user avatar
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 ...
cody's user avatar
  • 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) ...
Raphael's user avatar
  • 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$...
sai's user avatar
  • 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 ...
D.W.'s user avatar
  • 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 ...
Joey Eremondi's user avatar
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 ...
D.W.'s user avatar
  • 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 ...
D.W.'s user avatar
  • 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"...
Natalie Clarius's user avatar
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 ...
marc's user avatar
  • 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$$
John L.'s user avatar
  • 39.1k
2 votes

"Term Rewriting and All That" - Exercise 2.3

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 ...
D.W.'s user avatar
  • 162k

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