Questions tagged [rewriting-systems]
For questions related to (term) rewriting systems (which are reduction systems in which rewrite rules apply to terms).
32
questions
2
votes
1
answer
64
views
Mitchell Foundations for PL 2.3.4 (observational equivalence)
Background.
The language is PCF, with observable types $\text{bool}$ and $\text{nat}$.
$\text{eval}$ is the partial function on PCF terms such that $\text{eval}(M) = N$ iff $N$ is the unique normal ...
- 700
1
vote
1
answer
73
views
Equivalence of "compatible relation" definitions
$\newcommand{\abstraction}[2]{\lambda #1. #2}$
$\newcommand{\application}[2]{\left(#1 #2\right)}$
$\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$
$\newcommand{\freevars}[1]{\operatorname{FV}\...
- 21
2
votes
0
answers
33
views
Associahedron, but with swaps
The associahedron has edges of the form $a(bc)\rightarrow (ab)c.$ But I also want to include the possibility of swapping adjacent entries by doing operations like $a(bc) \rightarrow a(cb).$ I was ...
- 1,659
1
vote
1
answer
63
views
Convertibility of Two Lambda Expressions Equivalent to Existence of a Common Reduct
Suppose $\rightarrow$ is $\rm{\beta}$ reduction and $\twoheadrightarrow$ denotes a reduction sequence from $\rm{\beta}$ reductions. Convertibility of two lambda expressions is defined as follows: two ...
- 1,880
2
votes
1
answer
116
views
Missing parentheses in $s(k (s I I))(s(\lambda y. s(k y))(\lambda y. s I I)$ leads to interesting error in an nLab page. Need a double check.
I think I found an error in the nLab page on partial combinatory algebra in the Example combinators section:
Finally, consider the classical construction of the fixed-point combinator, $Y = \lambda y....
- 1,527
0
votes
1
answer
54
views
How does confluence apply (or not) in non-terminating rewriting systems?
Suppose we have the rules $\{x\to Ax, x \to xB\}$. We start with letting $x$ be the empty string, and are free to apply either rule at will. This will allow us to build any string of form $A^mB^n$.
...
- 6,046
0
votes
1
answer
97
views
Rewriting quadratic expression
I am currently learning how to factorise quadratic expressions of the form $ax^2 + bx + c$.
In my textbook (Foundations math seventh edition) they are elaborating on a particular way of finding a ...
- 11
2
votes
0
answers
56
views
Fewest applications of associativity
By repeatedly applying the basic associativity law $(x+y)+z = x+(y+z)$, one can get from any one expression with binary addition to any other with the variables in the same order.
Specifically, given ...
- 3,172
1
vote
1
answer
74
views
Question about number of occurences of a function symbol in a Term Rewriting System
While studying Termination of term rewriting systems I came across the folowing problem from Baader's book Term Rewriting and All That
$\textbf{My idea:}$
Let $s\rightarrow_R t$, then there exists $p\...
- 91
2
votes
1
answer
105
views
Non-identifiability of a periodic function
This paper (Page 657, Section 2.3) says:
It is well known that for a given function there might be more than one representation. For example, a purely harmonic function can also be represented as a ...
- 277
0
votes
1
answer
86
views
Is it possible to add computational facilities to otherwise "mathematical" formal systems by adjoining identities to types?
The following thought has been on my mind for years.
Think of $\mathbb{N}$ as the type of all well-formed expressions representing natural numbers. And think of $$\tilde{\mathbb{N}} := \frac{\mathbb{N}...
- 68.4k
2
votes
1
answer
49
views
Does $T(\Sigma,V)$, the set of terms for signature $\Sigma$ and a set $V$ of variables, belong to syntax or semantics?
Universal algebra has syntax and semantics parts.
A signature $\Sigma$ belongs to syntax.
Does $T(\Sigma,V)$, the set of terms for signature $\Sigma$ and a set $V$ of variables, belong to syntax or ...
- 48k
3
votes
2
answers
1k
views
What do "soundness" and "completeness" mean?
Soundness and completeness seem to occur in multiple scenarions:
In mathematical logic they are used to describe the
relationship between syntax and semantics of logic systems.
In relational ...
- 48k
1
vote
1
answer
60
views
Does $x \leftrightarrow^* y$ already imply $x \rightarrow^* y$?
In Baader's Term rewriting and all that:
Corollary 2.1.6 If $\rightarrow$ is confluent and $x \leftrightarrow^* y$ then
$x \rightarrow^* y$ if $y$ is in normal form, and
$x = y$ if both $x$ and $y$ ...
- 48k
0
votes
1
answer
70
views
Why does $y \downarrow x$ imply $ x \leftrightarrow^* y$?
In Baader's Term rewriting and all that:
Definition 2.1.3 A reduction $\rightarrow$ is called
Church-Rosserf iff $ x \leftrightarrow^* y \Rightarrow y \downarrow x$
Because $y \downarrow x$ implies $...
- 48k
1
vote
1
answer
687
views
What are the relations and differences between formal systems, rewriting systems, formal grammars and automata?
I learned from Herre & Schroeder-Heister's "Formal Languages and Systems" that
A formal system is based on a formal language $L$, endowing it with a consequence
operation $C: 2^L\to 2^...
- 48k
0
votes
0
answers
49
views
Homological invariance met03
In the following article
https://hal.archives-ouvertes.fr/hal-00148349/document
at the end of the proof of theorem 6.1 (p. 167), the author writes that he can conclude thanks to familiar ...
- 11
0
votes
0
answers
105
views
Combinatorial applications of diamond lemma
Recently, I found the following presentation by Darij Grinberg about applications of diamond lemma. Here is the link:
http://www.cip.ifi.lmu.de/~grinberg/algebra/diamond-talk.pdf
It seems to be very ...
- 4,322
4
votes
1
answer
78
views
Uniqueness of the result of rewritting an algebraic expression using distributivity rule
Let $expr$ be an algebraic expression involving natural numbers, addition operator and multiplication operator, e.g.,
$$(1+2)\cdot(3+4 \cdot 5)+6.$$
By iteratively applying the distributivity of ...
- 151
1
vote
0
answers
30
views
If a relation is terminating, then well-founded induction holds.
Proposition: If the relation $\to$ is terminating, then well-founded induction holds.
ProofAttempt:
If $\to $ terminates, then $\exists$ no infinite descending chains such as $a_0 \to a_1 \to \cdots$....
- 1,788
0
votes
1
answer
31
views
Formula Rearrangement
Hi StackExchange community,
The formula has this form:
$$ {-7 \pm X \over \sqrt{2} - 3}-3.$$
How can I rewrite this to be more compact ?
Thank you.
- 329
0
votes
1
answer
32
views
Need help isolating variables (average translational energy equation)
I need to rewrite equation so that i can use gamma function. Below are assignment text and my steps and reasoning so far:
The probability of finding a translational energy in the range
$$E_{tr}, ...
6
votes
2
answers
105
views
In rewiring systems do definitions creates new rewrite laws or an alias? And is this a meaningful question?
Lambda calculus is often introduced as a rewriting or substitution system. Where $\beta$ reduction is described as replacing bound variables with the value that variable is bound to. For example $(\...
- 4,647
2
votes
1
answer
115
views
a locally confluent and terminatting rewrite system is complete
I want to prove that every locally confluent rewrite system is confluent. Since I know very little about rewrite systems and logic, I tried looking at it as a digraph with no external infinite paths ...
- 897
2
votes
4
answers
12k
views
What is this constant 'C' in integration? Why is it different when I integrate using different techniques?
Method 1:
Method 2:
In these two images, you will see that I have integrated $\sin^3 x$ using different techniques. As you can see I get different answers. I asked my teacher why this is and he said ...
2
votes
1
answer
87
views
A question about a confluent abstract rewriting system?
Let $(A,\rightarrow)$ be a confluent abstract rewriting system. Assume that $a\stackrel{*}\rightarrow b$, $a\stackrel{*}\rightarrow c$ is a fork. Then $b,c$ is joinable, that is, there is a $d\in A$ ...
- 984
1
vote
1
answer
386
views
How to extract PID parameters from a controller in zpk form?
I have a plant of 3th order, e.g.:
$$
G(s)=\frac{5}{(s+2)(s^2+2s+4)}
$$
that I want to control by tracking the reference.
Now I need to have a fast response, zero steady-state error and low overshoot. ...
- 147
1
vote
1
answer
233
views
A question about how to check a rewriting system is confluent?
I am reading the book "Computation with finitely presented groups" on page 59,
I don't know why we need only test six words? does any other words can be generated by the six words? it is seems not.
- 984
2
votes
1
answer
27
views
Special Sequences, homework
I'm preparing for my mathematics exam and I am stuck on something which I believe should be simple. The question is as follows:
A rough estimate of the total oil and gas reserves of a country at the ...
- 87
1
vote
1
answer
92
views
Prove confluence
I have these 2 questions to prove or disprove confluence.
1)
Answer
2)
Answer
Now I am having difficulty understanding these. Aren't these 2 questions same? then why in one case it is confluent ...
- 155
3
votes
1
answer
639
views
Consequences of difference between "strong" and weak Church-Rosser property
An Abstract rewriting system is a set A, whose elements are usually
called objects, together with a binary relation on A, traditionally
denoted by $\rightarrow$.
An object $x \in A$ is called ...
5
votes
1
answer
327
views
Bergman's Diamond Lemma: do these rules lead to a normal form?
Last week I was recommended Bergman's Diamond Lemma in these comments. I read through the paper, and was working on an exercise in it on page 193:
Examine for termination each of the following ...
- 2,735