reference on relating Post systems to string rewriting systems and formal grammars?

wikipedia states:

Every Post canonical system can be reduced to a string rewriting system (semi-Thue system) […] It has been proved that any Post canonical system is reducible to such a substitution system, which, as a formal grammar, is also called a phrase-structure grammar, or a type-0 grammar in the Chomsky hierarchy

and on a different page:

A semi-Thue system is also a special type of Post canonical system, but every Post canonical system can also be reduced to an SRS.

I have not been able to find much explanation of these statements.

Is there a good reference that shows how to do conversions between these notions?

Proving a first order logic theorem with equational logic with a term rewriting system

I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean Algebra). The target language also permits Skolemization (Sk). So the translation task is from FOL to EL+BL+Sk. My motivation is that if my translation and subsequent proof in EL+BL+Sk are correct, then I should be able to perform such proofs using a Term Rewriting System (TRS). TRS can be used to prove equational theories. Because EL+BL is a sub-logic of FOL and Skolemization results in an equisatisfiable system, it is hoped that a valid proof in EL+BL+Sk is a valid proof of the original FOL theorem. Below is a FOL example and my attempt at a proof using natural deduction. This is followed by my attempt at translation and proof in EL+BL+Sk. See notes on translation/proof below.

My questions are:

Is the tentative translation from FOL to EL+BL+Sk correct?

Is the tentative proof in EL+BL+Sk correct?

Does the proof in EL+BL+Sk count as a proof of the original FOL theorem? I am not sure how proof theoretic entailment ($ \vdash$ ) in FOL relates to semantic entailment ($ \models$ ) in EL+BL+Sk. Does ($ \Gamma \models_{EL+BL+Sk} \varphi \iff \Gamma \vdash_{FOL} \varphi$ ) hold?

Example FOL formulae

At least one person is liked by every person: $ \exists y \forall x :Likes(x,y)$

Every persons likes at least one person: $ (\forall x \exists y: Likes(x,y)) $

I want to prove: $ (\exists y \forall x: Likes(x,y)) \vdash (\forall x \exists y : Likes(x,y)) $

Natural Deduction (ND) proof

enter image description here

The ND proof uses syntactic consequence where $ \Gamma \vdash \varphi$ means that the sentence $ \varphi$ is provable from the set of assumptions $ \Gamma$ . \begin{align*} &\textbf{FOL Theorem}~~(\exists y \forall x :Likes(x,y)) \vdash (\forall x \exists y :Likes(x,y)) \ &\ &\textbf{Notation for EL+BL+Sk}\ &x~~~~~~~~~~~~~~~~~~~~~~~~~\forall x~~\text{Universally Quantified variable}\ &c~~~~~~~~~~~~~~~~~~~~~~~~~~\text{Skolem Constant}\ &d~~~~~~~~~~~~~~~~~~~~~~~~\text{Arbitrary $ Person$ , for universal elimination}\ &\mathtt{skFun}~~~~~~~~~~~~~~~~\text{Skolem Function}\ &\mathtt{Likes}~~~~~~~~~~~~~~~~\text{Boolean valued function}\ &\mathtt{true}~~~~~~~~~~~~~~~~~~\text{Boolean constant}\ &\ &\textbf{Translation of Theorem to EL+BL+Sk:}\ &(\forall x :(\mathtt{skFun}(x)=c ,\mathtt{Likes}(x,c)))\models(\forall x:\mathtt{Likes}(x,\mathtt{skFun}(x))) \ &\ &\textbf{Proof in EL+BL+Sk}\ &\textbf{1}~~\forall x:\mathtt{Likes}(x,c) = true~~~~~~\text{Assumption, with Skolem constant $ c$ }\ &\textbf{2}~~\forall x:\mathtt{skFun}(x) = c~~~~~~~~~~~~~~~\text{Interpretation of Sk. function with Sk. constant $ c$ }\ &\textbf{3}~~\mathtt{Likes}(d,\mathtt{skFun}(d))~~~~~~~~~~~~\text{Universal elim & Skolemization of term to be proved}\ &\textbf{4}=~~~~~\mathtt{Likes(d,c)}~~~~~~~~~~~~~~~~\text{Apply 2 to second argument of 3}\ &\textbf{5}=~~~~~~true~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\text{Apply 1 at 4}\ \end{align*} Notes on translation/proof.

  • The EL+BL+Sk proof relies on an interpretation, so the translation needs semantic entailment $ \models$ . In general, this can be written as $ \Gamma \models_{EL+BL+Sk} \varphi$ , which means that under $ EL+BL+Sk$ logic the sentence $ \varphi$ is true in all models of $ \Gamma$ .

  • In EL all variables are considered to be universally quantified.

  • Existential variables in FOL that are not in the scope of universals are translated to Skolem constants.

  • Existential variables in FOL that are in the scope of universals are translated to Skolem functions e.g. $ \mathtt{skFun}(x)$ with single universal argument of $ x$ . The original existential was in the scope $ x$ .

  • Each predicate in FOL is translated to a Boolean valued operation in EL+BL+Sk, e.g. predicate $ Likes$ becomes Boolean operation $ \mathtt{Likes}$ .

  • In EL terms are distinct, unless they are made identical or equal by equations.

Here is the listing in CafeOBJ using TRS.

mod LIKES {   [Person]   pred Likes : Person Person         }  op c : -> Person . ops d : -> Person . op skFun : Person -> Person . -- Hypothesis  eq [assumption] : Likes(x:Person,c) = true . eq [skolem] :  skFun(x:Person) =  c . reduce Likes(d,skFun(d)) . --> Gives true 

Right filter for rewriting page statuscode

I am new to developing wordpress plugins. But I am looking to write a fairly simple plugin.

I want to write a plugin that rewrites the returned status code based on some logic that consults a database. It can essentially be boiled down to an access plugin based on custom logic. When authorization fails I want to either return statuscode 403 or redirect to a login page.

But I am struggling to find the right place to hook in. And also the “correct” way of doing it.

The logic is based on a combination of the Page requested, the logged in user and that users role. Using these values I look up information in a database and either render some custom data or want to turn the user away. If the user is logged in I want to return a 403 but if the user is not logged in I want to return a 401. But is that even the right way of doing it in WordPress? I am used to writing APIs and have never written a WordPress plugin.

Should I render a text that says Content not available! instead of a 403 and redirect the user to the login page instead of a 401?

Ideally I would like to separate the logic that renders the data and the logic that authorizes. I would like that to be two different hooks or filters.

I have tried to add a filter on http_response but I can’t get it to do anything. I am in doubt if I should call apply_filter myself or if WordPress does that.

All help is appreciated.

Rewriting URL path in nginx without redirecting

For legacy reasons, I have URLs like I want /foo.cgi?id=nnn.html to respond with the contents of a file nnn.html, where nnn is a number that varies.

In nginx, how do I define a custom mapping from URL paths to different file paths without generating redirects? (That is, while I want the contents of nnn.html to be served, I want the browser-visible URL to continue to be foo.cgi?id=nnn.)

Dovecot Configuration: rewriting / key→value lookup for variables; aliasing the domain

I’d like to configure Dovecot in a way so that it dispatches userdb/passwd lookups into domain specific locations, where the domain itself may have several aliases, but all of them direct to the same location.

The Dovecot wiki gives a simple, trivial example

Multiple passwd files

You can use all the variables in the passwd-file filenames, for example:

passdb {   driver = passwd-file   # Each domain has a separate passwd-file:   args = /etc/auth/%d/passwd } 

However this does not take care of the domain aliasing that may take place. For example a company might have the domains and, and would like to alias them to all work with the same file /site/example/mail/passwd.

Assuming the above example, it would require to rewrite the %d variable through some alias lookup or to first alias the domain, before moving on to look up the user and authenticating.

Now I do understand that Dovecot doesn’t treat the domain part in any special way, so I could users just have configure their MUAs using the joint domain alias. However this doesn’t deal with domain aliasing on delivery.

Ideally I could insert some lookup to rewrite the domain part early on, to be used for delivery and authentication. However I don’t see how to do that without crude hacks.

Rewriting ‘From:’ in ssmtp/mail no longer works in Ubuntu 18.04

In Ubuntu 14.04 I had the following system running which is basically described here and also here. One element of this is that the ‘From:’ address is taken from /etc/ssmtp/revaliases: 

and the ‘’ was used as ‘From:’ when I issued a mail like echo -e “Hi there” | mail -s Test

In a new installation of Ubuntu 18.04, the ‘From:’ is now

 Clearname <username@hostname> 

where clearname is the name string in /etc/passwd, username is the linux username, and hostname is the linux host name (although changing it with ‘hostname’ does not alter the result).

Of course, this e-mail address is not going to work, I would like to supply my real address. It seems like new versions of GMail or SSMTP have broken this useful and essential feature.

I would be grateful for help!

Rewriting complex formal derivatives

Formal derivatives are given by the following formulas

\begin{align} \frac{\partial f}{\partial z} = \frac{1}{2} \bigg( \frac{\partial f}{\partial x} – i\frac{\partial f}{\partial y} \bigg) \ \frac{\partial f}{\partial \overline{z}} = \frac{1}{2} \bigg( \frac{\partial f}{\partial x} + i\frac{\partial f}{\partial y} \bigg) \end{align} I am to rewrite $ $ \frac{\partial \overline{f}}{\partial z}$ $ and $ $ \frac{\partial \overline{f}}{\partial \overline{z}}$ $

How can it be done? Am I to use Riemann — Cauchy equations? If yes how?