Questions tagged [rewriting]

Repeatedly applying rules to transform objects

From Wikipedia:

In mathematics, computer science, and logic, rewriting covers a wide range of (potentially non-deterministic) methods of replacing subterms of a formula with other terms. What is considered are rewriting systems (also known as rewrite systems or reduction systems). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

Rewriting can be non-deterministic. One rule to rewrite a term could be applied in many different ways to that term, or more than one rule could be applicable. Rewriting systems then do not provide an algorithm for changing one term to another, but a set of possible rule applications. When combined with an appropriate algorithm, however, rewrite systems can be viewed as computer programs, and several declarative programming languages are based on term rewriting.

116 questions
26
votes
3 answers

Rewriting as a practical optimization technique in GHC: Is it really needed?

I was reading the paper authored by Simon Peyton Jones, et al. named “Playing by the Rules: Rewriting as a practical optimization technique in GHC”. In the second section, namely “The basic idea” they write: Consider the familiar map function, that…
Aadit M Shah
  • 72,912
  • 30
  • 168
  • 299
16
votes
1 answer

How does term-rewriting based evaluation work?

The Pure programming language is apparently based on term rewriting, instead of the lambda-calculus that traditionally underlies similar-looking languages. ...what qualitative, practical difference does this make? In fact, what is the difference in…
Alex Celeste
  • 12,824
  • 10
  • 46
  • 89
10
votes
2 answers

Use of term rewriting in decision procedures for bit-vector arithmetic

I am working on a project whose focus is the use of term rewriting to solve/simplify fixed-size bit-vector arithmetic problems, which is something useful to do as a prior step to some decision procedure such as those based on bit-blasting. The term…
iago
  • 277
  • 1
  • 10
7
votes
1 answer

LYAH - Understanding comment about "tell" when chaining Writer monads

Question is in bold at the bottom. LYAH gives this example of using the do notation with the Writer monad import Control.Monad.Writer logNumber :: Int -> Writer [String] Int logNumber x = writer (x, ["number " ++ show x]) multWithLog :: Writer…
Enlico
  • 23,259
  • 6
  • 48
  • 102
7
votes
2 answers

Rewriting network packets on the fly using libnetfilter_queue

I am attempting to write a userspace application that can hook into an OS's network stack, sniff packets flying past and edit ones that its interested in. After much Googling, it appears to me that the simplest (yet reasonably robust) method of…
Aidan Steele
  • 10,999
  • 6
  • 38
  • 59
7
votes
4 answers

Do I need to write my own unmanaged IL library to rewrite IL with the CLR Profiling API?

I've been looking at some of the articles for the CLR Profiling API, and many of those articles talk about calling SetILFunctionBody() to do the actual IL rewriting; however, none of those articles actually explain exactly what you could use to…
plaureano
  • 3,139
  • 6
  • 30
  • 29
6
votes
1 answer

How to rewrite over Rle inside a term with Rmult in Coq?

With respect to the relation Rle (<=), I can rewrite inside Rplus (+) and Rminus (-), since both positions of both binary operators have fixed variance: Require Import Setoid Relation_Definitions Reals. Open Scope R. Add Parametric Relation : R…
Daniel
  • 71
  • 2
4
votes
1 answer

Coq: rewriting under if-then-else

I sometimes need to apply a simplification in a branch of an if-then-else without destructing the discriminee. From Coq Require Import Setoid. Lemma true_and : forall P, True /\ P <-> P. Proof. firstorder. Qed. Goal (forall (b:bool) P Q, if b…
pjm
  • 269
  • 1
  • 8
4
votes
2 answers

URL Rewriting not work on Wamp Server

I've a problem with Wamp Server and URL Rewriting. I've import my project from production server with his .htaccess. The URL Rewriting work fine on production, but not in localhost. In my Wamp configuration, rewrite_module is activate. In the…
Nowis
  • 392
  • 3
  • 16
4
votes
1 answer

Shunting Yard Algorithm with Variables

I'm currently working on a modified version of the Shunting Yard Algorithm that would work with variables, but I cant figure out how to get it to work. For example, I would want the algorithm to re-write 2 * (2x + 5) - 5 to 4x + 5. Any ideas / links…
Alston Lin
  • 197
  • 4
  • 10
3
votes
1 answer

Rewriting mulitple URLS

I am trying to rewrite different URLs. The first three lines work, but lower ones do not. I get a 500 Internal Server Error. A snippet of my htaccess file: RewriteCond %{SCRIPT_FILENAME} !-d RewriteCond %{SCRIPT_FILENAME} !-f RewriteRule ^word/(.*)$…
Andreas
  • 41
  • 4
3
votes
1 answer

Algebraic Simplification on Abstract Syntax Tree

I've designed a parser in C that is able to generate AST, but when I begin to implement simplifications it really got messed up. I've successfully implemented rules for the summation below; x + 0 -> x x + x -> 2 * x etc. But it took huge amount of…
Arif Balik
  • 115
  • 1
  • 9
3
votes
1 answer

Agda: rewriting instead of explicit coercion in type definition?

When dealing with equalities on types in Agda, it is often necessary to coerce the inhabitants the types using a hand-made coercion like coerce : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B coerce refl x = x It was discussed here that explicit coercion of…
Simon Forest
  • 133
  • 2
3
votes
1 answer

ASP.NET Core 2 Url Rewriting middleware to redirect from .xxx to .yyy extension

I want to redirect all request from .com to .net with the same path and route in dot net core. Same as below code for removing www from start URL: app.UseRewriter(new RewriteOptions().Add(ctx => { // checking if the hostName has www. at the…
3
votes
1 answer

Second order unification with rewrite

I have a lemma such as the following, with a higher-order parameter: Require Import Coq.Lists.List. Lemma map_fst_combine: forall A B C (f : A -> C) (xs : list A) (ys : list B), length xs = length ys -> map (fun p => f (fst p)) (combine xs…
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
1
2 3 4 5 6 7 8