Questions tagged [rewriting-systems]
For questions related to (term) rewriting systems (which are reduction systems in which rewrite rules apply to terms).
33
questions
0
votes
0
answers
29
views
Why when rewriting a second order diff. equation as a first order equation with dependent variable $\theta\in S^1$ must $d\theta/dt=v\in \mathbb{R}$?
I apologise for this simple question and I am sure what I am missing here is quite obvious. I completed a question earlier in which I had to rewrite the differential equation
$d^2\theta/dt^2+\delta d\...
- 23
1
vote
1
answer
49
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
0
votes
0
answers
19
views
How to I impose the parameterization $0\leq \alpha \leq \beta <1$?
I want to restrict values s.t. I get $\theta = (\alpha, \beta) =g(\theta_1, \theta_2)$
with the following restrictions.
$
0\leq \alpha \leq \beta <1
$
I know the correct answer should be $\beta = (...
- 35
2
votes
0
answers
31
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,505
1
vote
1
answer
55
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,796
2
votes
1
answer
109
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,427
0
votes
1
answer
45
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$.
...
- 5,739
0
votes
1
answer
89
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
54
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 ...
- 2,722
1
vote
1
answer
63
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
104
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
81
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}...
- 67.2k
2
votes
1
answer
46
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 ...
- 46.7k
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 ...
- 46.7k
1
vote
1
answer
55
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$ ...
- 46.7k
0
votes
1
answer
67
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 $...
- 46.7k
1
vote
1
answer
554
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^...
- 46.7k
0
votes
0
answers
48
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
94
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,032
3
votes
1
answer
75
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 ...
- 141
1
vote
0
answers
25
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,748
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.
- 319
0
votes
1
answer
28
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
99
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,540
2
votes
1
answer
99
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
11k
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
81
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
350
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
173
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
26
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
89
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
557
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
320
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,715