Questions tagged [rewriting-systems]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2
votes
1answer
94 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 ...
0
votes
1answer
57 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}...
2
votes
1answer
21 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 ...
1
vote
2answers
100 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 ...
1
vote
1answer
32 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$ ...
0
votes
1answer
47 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 $...
0
votes
1answer
85 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^...
0
votes
0answers
47 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 ...
1
vote
0answers
58 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 ...
3
votes
1answer
62 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 ...
1
vote
0answers
11 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$....
0
votes
1answer
28 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.
0
votes
1answer
25 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
2answers
84 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 $(\...
1
vote
1answer
31 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 ...
2
votes
4answers
5k 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
1answer
51 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$ ...
1
vote
1answer
153 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. ...
1
vote
1answer
79 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.
2
votes
1answer
21 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 ...
1
vote
1answer
52 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 ...
3
votes
1answer
369 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
1answer
291 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 ...