Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.compilers > #1265 > unrolled thread

Formatting of Language LRMs

Back to article view | Back to comp.compilers

Contents

  Formatting of Language LRMs Seima Rao <seimarao@gmail.com> - 2014-06-17 16:54 +0530
    Re: Formatting of Language LRMs "lpsantil@gmail.com" <lpsantil@gmail.com> - 2014-06-20 10:10 -0700
      Re: Formatting of Language LRMs glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2014-08-03 04:37 +0000
    Re: Formatting of Language LRMs Ivan Godard <ivan@ootbcomp.com> - 2014-06-20 12:09 -0700
      Re: Formatting of Language LRMs glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2014-06-21 02:27 +0000
      Re: Formatting of Language LRMs Kaz Kylheku <kaz@kylheku.com> - 2014-06-21 03:09 +0000
      Re: Formatting of Language LRMs Joshua Cranmer 🐧 <Pidgeot18@verizon.net.invalid> - 2014-06-22 21:12 -0500
        Re: VWG and K, was Formatting of Language LRMs Ivan Godard <ivan@ootbcomp.com> - 2014-06-22 21:47 -0700
        RE: Formatting of Language LRMs "Costello, Roger L." <costello@mitre.org> - 2014-07-03 09:06 +0000
          Re: Formatting of Language LRMs Ivan Godard <ivan@ootbcomp.com> - 2014-07-03 22:30 -0700
            Re: syntax checkers, was Formatting of Language LRMs glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2014-07-04 17:35 +0000
            Re: executable semantics, was Formatting of Language LRMs wclodius@earthlink.net (William Clodius) - 2014-07-04 15:53 -0600
    Re: specifying semantics, was Formatting of Language LRMs seimarao@gmail.com - 2014-06-24 02:19 -0700
      Re: specifying semantics, was Formatting of Language LRMs "lpsantil@gmail.com" <lpsantil@gmail.com> - 2014-06-24 13:12 -0700
      Re: specifying semantics, was Formatting of Language LRMs George Neuner <gneuner2@comcast.net> - 2014-06-26 00:54 -0400
        Re: specifying semantics, was Formatting of Language LRMs Andy Walker <news@cuboid.co.uk> - 2014-06-28 20:10 +0100
          Re: specifying semantics, was Formatting of Language LRMs George Neuner <gneuner2@comcast.net> - 2014-06-28 22:43 -0400
            Re: BNF, was specifying semantics wclodius@earthlink.net (William Clodius) - 2014-06-30 22:00 -0600
        Re: specifying semantics, was Formatting of Language LRMs Ivan Godard <ivan@ootbcomp.com> - 2014-06-28 12:25 -0700
          Re: specifying semantics, was Formatting of Language LRMs Andy Walker <news@cuboid.co.uk> - 2014-06-29 11:19 +0100
          Re: specifying semantics, was Formatting of Language LRMs George Neuner <gneuner2@comcast.net> - 2014-06-29 07:56 -0400
            Re: specifying semantics, was Formatting of Language LRMs Ivan Godard <ivan@ootbcomp.com> - 2014-06-29 11:49 -0700
              Re: specifying semantics, was Formatting of Language LRMs Gene Wirchenko <genew@telus.net> - 2014-06-30 18:09 -0700
                Re: specifying semantics, was Formatting of Language LRMs Ivan Godard <ivan@ootbcomp.com> - 2014-06-30 20:53 -0700
                  Re: Algol history, was specifying semantics anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2014-07-03 11:51 +0000
                    Re: Algol history, was specifying semantics Ivan Godard <ivan@ootbcomp.com> - 2014-07-03 22:20 -0700
                    Re: Algol history, was specifying semantics wclodius@earthlink.net (William Clodius) - 2014-07-04 15:52 -0600
                      Re: Algol history, was specifying semantics glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2014-07-07 05:49 +0000
                        Re: Algol history, was specifying semantics Ivan Godard <ivan@ootbcomp.com> - 2014-07-07 10:48 -0700
                          Re: Algol history, was specifying semantics glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2014-07-07 19:49 +0000
                        Re: Algol history, was specifying semantics glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2014-07-07 19:43 +0000
                  Re: specifying semantics, was Formatting of Language LRMs Gene Wirchenko <genew@telus.net> - 2014-07-03 21:44 -0700
              Re: specifying semantics, was Formatting of Language LRMs anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2014-07-02 09:51 +0000
                Re: specifying semantics, was Formatting of Language LRMs Stefan Monnier <monnier@iro.umontreal.ca> - 2014-07-03 10:15 -0400
                  Re: specifying semantics, was Formatting of Language LRMs glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2014-07-04 06:08 +0000
                  Re: specifying semantics, was Formatting of Language LRMs Hans-Peter Diettrich <DrDiettrich1@aol.com> - 2014-07-04 08:51 +0200
                    Re: Parsing Fortran, was specifying semantics glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2014-07-04 17:53 +0000
                      Re: Parsing Fortran, was specifying semantics wclodius@earthlink.net (William Clodius) - 2014-07-04 15:57 -0600
    Re: Formatting of Language LRMs mertesthomas@gmail.com - 2014-06-30 12:04 -0700
    Re: Formatting of Language LRMs federation2005@netzero.com - 2014-07-28 17:55 -0700
      Re: Formatting of Language LRMs federation2005@netzero.com - 2014-08-01 14:58 -0700

Page 1 of 3  [1] 2 3  Next page →

#1265 — Formatting of Language LRMs

Hi,

    We are in a great era of infinite languages and sure standardizations.

   I myself keep studying a same few standards whenever there is free time.

   Some of the noticeable aspect about standards is that most of them
   tend to follow the same format: grammar in BNF, semantics in
   documentation. This is the pattern throughout.

   Therefore I am curious to know if there are other interesting formatting
   of language standards or language definitions such that the
   pattern is different?

    This sounds crazy but language designers tend to be geeky hence
   the curiousity.

Sincerely,
Seima Rao.
[People have tried lots of other definition schemes over the years, like railroad
diagrams in some Fortran standards and VDL in PL/I.  BNF+text seems to be a workable
balance between formalisms and readability. The PL/I standard was notably opaque,
and its authors said "you don't have to understand it, just implement it" to which
the answer was "yeah, bugs and all." -John]

[toc] | [next] | [standalone]

#1268

Personally, I enjoy Wirth Syntax Notation (WSN)[1] more than BNF/EBNF.
There are wikipedia entries, I believe, also incorrectly identifies
the PL/0 language grammar (also Wirth's work)[2][3] as EBNF when it is
WSN.

[1] http://en.wikipedia.org/wiki/Wirth_syntax_notation
[2] http://en.wikipedia.org/wiki/Recursive_descent_parser
[3] http://en.wikipedia.org/wiki/PL/0

[toc] | [prev] | [next] | [standalone]

#1359

lpsantil@gmail.com <lpsantil@gmail.com> wrote:
> Personally, I enjoy Wirth Syntax Notation (WSN)[1] more than BNF/EBNF.
> There are wikipedia entries, I believe, also incorrectly identifies
> the PL/0 language grammar (also Wirth's work)[2][3] as EBNF when it is
> WSN.

After a previous post, it occurred to me that a tool that would
convert yacc input into printable BNF might be useful. That way,
the printed version would agree with the compiled version.

> [1] http://en.wikipedia.org/wiki/Wirth_syntax_notation
> [2] http://en.wikipedia.org/wiki/Recursive_descent_parser
> [3] http://en.wikipedia.org/wiki/PL/0

-- glen
[I'm not sure how useful it would be, since most practical yacc
grammars use precedence and other hacks to accept a language
that's not the same as the mechanically generated BNF would. -John]

[toc] | [prev] | [next] | [standalone]

#1271

On 6/17/2014 4:24 AM, Seima Rao wrote:
>     Some of the noticeable aspect about standards is that most of them
>     tend to follow the same format: grammar in BNF, semantics in
>     documentation. This is the pattern throughout.
>
>     Therefore I am curious to know if there are other interesting formatting
>     of language standards or language definitions such that the
>     pattern is different? ...

> [People have tried lots of other definition schemes over the years, like railroad
> diagrams in some Fortran standards and VDL in PL/I.  BNF+text seems to be a workable
> balance between formalisms and readability. The PL/I standard was notably opaque,
> and its authors said "you don't have to understand it, just implement it" to which
> the answer was "yeah, bugs and all." -John]

Two very important cases not following this practice: Algol68, which
used van Wijngaarten notation ("VWG"), and Ada where the standard is
defined by a test suite. There are Ada manuals, but if the manual
differs from the suite then the suite governs.

VWG is vastly superior to BNF because it provides a formal specification
of semantics, in particular the type system, which cannot be expressed
in BNF. Unfortunately formal reasoning about semantics is beyond many
users. Stll IMO no other formal semantic notation (Denotational
Semantics for example) is superior to VWG.

The Ada approach was driven by the government procurement process in
which they had too much experience with ambiguous specification and
differing, incompatible implementations,. They sought a mechanism by
which they could have some confidence that their programs would
actually work with the same results in different environments, with
enforceable contracts that did not depend on the pissing contests of
language lawyers. This was largely successful, and Ada has a huge
canonical test suite. Other languages have evolved similar suites, and
in practice the major compilers run all their issues through each
others' compilers to produce an informal consensus, but that's not a
formal process.

[toc] | [prev] | [next] | [standalone]

#1274

Ivan Godard <ivan@ootbcomp.com> wrote:

(snip)

> Two very important cases not following this practice: Algol68, which
> used van Wijngaarten notation ("VWG"), and Ada where the standard is
> defined by a test suite. There are Ada manuals, but if the manual
> differs from the suite then the suite governs.

Not so long ago, regarding a question that I think was from this
group, but maybe a different one, I downloaded the Algol-68
description.  I could see that the information was there, but it was
too hard to figure out the answer to the question.

I have an actual book on Algol-60.

-- glen
[I had the same problem, the Algol68 language is great, but the
description is impenetrable. -John]

[toc] | [prev] | [next] | [standalone]

#1275

On 2014-06-20, Ivan Godard <ivan@ootbcomp.com> wrote:
> VWG is vastly superior to BNF because it provides a formal specification
> of semantics, in particular the type system, which cannot be expressed
> in BNF.

How do you put this into VWG, semantics and all:

  (lisp-macro with (mystery arguments))

:)

[toc] | [prev] | [next] | [standalone]

#1276

On 6/20/2014 2:09 PM, Ivan Godard wrote:
> VWG is vastly superior to BNF because it provides a formal specification
> of semantics, in particular the type system, which cannot be expressed
> in BNF. Unfortunately formal reasoning about semantics is beyond many
> users. Stll IMO no other formal semantic notation (Denotational
> Semantics for example) is superior to VWG.

I did a bit of playing with K during a course a few years ago, and I
ended up getting the feeling that the start of the art in executable
semantics is such that we could start seeing languages written as
executable semantics in maybe 10-20 years or so. While I did have a very
large share of swearing and screaming at the tool for its deficiencies,
I did leave the course actually feeling like I would want to use K if I
had the chance, which is more than I can say for the few other attempts
I've had at using formal methods tooling (disclaimer: the professor of
said course led the development of K).

Link: <http://www.kframework.org/index.php/Main_Page>.

--
Beware of bugs in the above code; I have only proved it correct, not
tried it. -- Donald E. Knuth

[toc] | [prev] | [next] | [standalone]

#1277 — Re: VWG and K, was Formatting of Language LRMs

> I did a bit of playing with K during a course a few years ago, and I
> ended up getting the feeling that the start of the art in executable
> semantics is such that we could start seeing languages written as
> executable semantics in maybe 10-20 years or so. While I did have a
> very large share of swearing and screaming at the tool for its
> deficiencies, I did leave the course actually feeling like I would
> want to use K if I had the chance, which is more than I can say for
> the few other attempts I've had at using formal methods tooling
> (disclaimer: the professor of said course led the development of K).
>
> Link: <http://www.kframework.org/index.php/Main_Page>.

I have never played with K, but after a run through the doc it appears
to have much the same goal as VWG, but to be more imperative/pattern
oriented and less applicative than VWG. Either will be a steep ramp.

Anyone can do syntax; sugar is easy, but also immoral and fattening.
Semantics is much harder, but worthwhile. Stretch those synapses!

[toc] | [prev] | [next] | [standalone]

#1294

> getting the feeling that the start of the art
> in executable semantics is such that we
> could start seeing languages written as
> executable semantics in maybe 10-20 years
> or so.

What are "executable semantics"?

If I were to create a document containing executable semantics, what would I do with it? How would it differ from a document containing, say, Java?

Fascinating discussion - thanks!

/Roger

[toc] | [prev] | [next] | [standalone]

#1299

On 7/3/2014 2:06 AM, Costello, Roger L. wrote:

> What are "executable semantics"?
>
> If I were to create a document containing executable semantics, what
> would I do with it?

You would apply it to a purported program and "execute" it and see if
you got diagnostics. Am executable spec is in effect the checking part
of a compiler.

How would it differ from a document containing,
> say, Java?

If the document were a compiler written in Java (i.e. a recognizer and
checker) then formally there is no difference. Practically, an immense
difference. VWG is an ASL for specifying languages. All of Algol68 in
VWG was about four pages of appendix; a compiler for Algol68 written in
Java would be much more than that, even after you strip out optimization
and code generation.

Also, the specification in VWG lends itself to use of metatools: make a
change to the grammar and verify that the revision is complete,
consistent and not redundant. Not something easy to do when the language
is expressed by a Java recognizer.

[toc] | [prev] | [next] | [standalone]

#1302 — Re: syntax checkers, was Formatting of Language LRMs

Ivan Godard <ivan@ootbcomp.com> wrote:

(snip)

> If the document were a compiler written in Java (i.e. a recognizer and
> checker) then formally there is no difference. Practically, an immense
> difference. VWG is an ASL for specifying languages. All of Algol68 in
> VWG was about four pages of appendix; a compiler for Algol68 written in
> Java would be much more than that, even after you strip out optimization
> and code generation.

There are programs written for OS/360 called "syntax checkers".
They are not compilers, but only enough of one to tell whether
the input is valid syntax in the specific language.

I never used the actual program, but the PLM (Program Logic Manual)
has the (I believe) BNF form for the language, unlike the normal
compiler manuals.

As far as I know, they were not normally used in batch systems, but
were for use by TSO.

Seems to me it should be possible to write a program that will
take BNF input, and a program that is supposed to be written in
that language, and will tell you whether or not it is.

-- glen

[That's basically what yacc and other parser generators do, they
compile BNF or something similar into a program that recognizes input
in the BNF.  Of course, for syntax checking you also have to tokenize
the input which is another whole can of worms. -John]

[toc] | [prev] | [next] | [standalone]

#1304 — Re: executable semantics, was Formatting of Language LRMs

Ivan Godard <ivan@ootbcomp.com> wrote:
> How would it differ from a document containing,
> > say, Java?
>
> If the document were a compiler written in Java (i.e. a recognizer and
> checker) then formally there is no difference. Practically, an immense
> difference. VWG is an ASL for specifying languages. All of Algol68 in
> VWG was about four pages of appendix; a compiler for Algol68 written in
> Java would be much more than that, even after you strip out optimization
> and code generation.
>
> Also, the specification in VWG lends itself to use of metatools: make a
> change to the grammar and verify that the revision is complete,
> consistent and not redundant. Not something easy to do when the language
> is expressed by a Java recognizer.

FWIW if I remember correctly a varient of that belief led the Modula II
standard to attempt to descibe the langauage using the Vienna Definition
Method. They hoped to verify the formal description automatically, but
they could not afford the commercial tools and the implementation of one
of the participants was not ready in time when they decided they had to
get it out the door.

[toc] | [prev] | [next] | [standalone]

#1278 — Re: specifying semantics, was Formatting of Language LRMs

Is there something for semantics as BNF is for grammars ?

What do the books on type systems, lambda calculus, etc, teach and
where are their topics applied ?

Sincerely,
Seima Rao.

[toc] | [prev] | [next] | [standalone]

#1279 — Re: specifying semantics, was Formatting of Language LRMs

On Tuesday, June 24, 2014 2:19:05 AM UTC-7, seim...@gmail.com wrote:
> Is there something for semantics as BNF is for grammars ?
>
> What do the books on type systems, lambda calculus, etc, teach and

You mention type systems and their analysis is one other formalism.
Another I thought of which is maybe an odd edge case are PEGs (Parsing
Expression Grammars).  They are non-ambiguous grammars and their
semantics are limited/defined in the "mother" language.  However, I
would argue that going from the semantics in a PEG to general semantic
"text/word/explanation" would be very difficult.

[toc] | [prev] | [next] | [standalone]

#1280 — Re: specifying semantics, was Formatting of Language LRMs

On Tue, 24 Jun 2014 02:19:05 -0700 (PDT), seimarao@gmail.com wrote:

>Is there something for semantics as BNF is for grammars ?

First, there is no canon BNF.  What we refer to as "Backus-Naur Form"
today is not the original used for Algol-58, but is BNF plus a handful
of widely accepted practical extensions - alternation set notation,
closure notation, etc. - which together is known as EBNF ('E' for
"extended") or sometimes "core" EBNF.

Core EBNF is easily (but not trivially) portable: every popular
grammar tool understands it in concept, but not every tool uses
exactly the same rule syntax.

In addition, nearly every tool extends core EBNF to enable its own
unique features.  Grammars taking advantage of any feature not in core
EBNF generally will not be portable (not trivially and possibly not
even easily) to a different tool.


To answer your question: No ... there really is nothing for semantics
that approaches the ubiquity of EBNF for grammars.  The closest thing
in practice is the lambda calculus, but there are multiple forms of
the calculus and you'll find that every author extends their chosen
form in some slightly different way.


Moreover, there are 3 broad categories of semantic description:
operational, denotational and axiomatic.  Lambda calculus really is
suitable only for expressing operational and/or denotational forms.
Axiomatic descriptions generally take the form of a propositional
algebra.

Historically, *most* languages have been described by operational
semantics alone, and the majority did not use any formal calculus to
do so.  The most common form of description is, in fact, text - in
conjunction with a "reference" implementation: a compiler or
interpreter against which new implementations can be compared.

Scheme, ML and Haskell are described by denotational semantics.  There
undoubtedly have been others but these are the ones I know offhand.

I'm not aware any languages that are described solely by axiomatic
semantics [possibly some of the declarative logic or theorem prover
languages, but I'm not very familiar with any of these].  AFAIHS,
axiomatic descriptions tend to be more for the developer of a compiler
than for the user of it.  When the language gets documented, it tends
to be using an operational or denotational description.


>What do the books on type systems, lambda calculus, etc, teach and
>where are their topics applied ?

Read some and find out.

George

[toc] | [prev] | [next] | [standalone]

#1281 — Re: specifying semantics, was Formatting of Language LRMs

On 26/06/14 05:54, George Neuner wrote:
> [...] What we refer to as "Backus-Naur Form"
> today is not the original used for Algol-58, [...].

	The report ["Preliminary Report of ACM-GAMM Committee
on an International Algebraic Language"] describing what we now
call Algol 58 did not use BNF.  Instead, the syntax is listed
as "forms";  eg,

   " D. Statements Sigma
   "    Closed and self-contained [blah-de-blah].
   "      Form: Sigma ~ begin Sigma; Sigma; ~~~ ~~~ ~~~; Sigma end
   "    A statement may be made identifiable by attaching to it
   "  a label L, [blah ...]
   "      Form: Sigma  ~ L: Sigma "

Backus proposed his system for "metalinguistic formulae" [as used
in the Algol 60 report] in 1959, and it was adopted by Naur, the
editor of the papers and the report defining Algol 60.

--
Andy Walker,
Nottingham.

[toc] | [prev] | [next] | [standalone]

#1283 — Re: specifying semantics, was Formatting of Language LRMs

On Sat, 28 Jun 2014 20:10:27 +0100, Andy Walker <news@cuboid.co.uk>
wrote:

>On 26/06/14 05:54, George Neuner wrote:
>> [...] What we refer to as "Backus-Naur Form"
>> today is not the original used for Algol-58, [...].

>Backus proposed his system for "metalinguistic formulae" [as used
>in the Algol 60 report] in 1959, and it was adopted by Naur, the
>editor of the papers and the report defining Algol 60.

Yup, I goofed:  BNF was Algol 60, not 58.

Incidentally, Naur didn't simply adopt Backus's forms, he made a
number of improvements.  There was a move early to call it Backus
Normal Form, but Naur's contribution was deemed significant enough
that it came to called Backus-Naur instead.

George

[toc] | [prev] | [next] | [standalone]

#1292 — Re: BNF, was specifying semantics

George Neuner <gneuner2@comcast.net> wrote:

> On Sat, 28 Jun 2014 20:10:27 +0100, Andy Walker <news@cuboid.co.uk>
> wrote:
>
> >On 26/06/14 05:54, George Neuner wrote:
> >> [...] What we refer to as "Backus-Naur Form"
> >> today is not the original used for Algol-58, [...].
>
> >Backus proposed his system for "metalinguistic formulae" [as used
> >in the Algol 60 report] in 1959, and it was adopted by Naur, the
> >editor of the papers and the report defining Algol 60.
>
> Yup, I goofed:  BNF was Algol 60, not 58.
>
> Incidentally, Naur didn't simply adopt Backus's forms, he made a
> number of improvements.  There was a move early to call it Backus
> Normal Form, but Naur's contribution was deemed significant enough
> that it came to called Backus-Naur instead.

Backus designed his initial version of BNF to describe the syntax of
Algol 58 for the International Conference on Information Processing of
UNESCO in 1959. Peter Naur in attending the conference was surprised
to discover that the syntax that Backus presented was different from
what he thought. He then examined the original report and discovered
that the desciption was ambiguous, and was compatible with both
Backus's and his interpretation. He also recognized that BNF would
allow an unambiguous description and adapted it for the Algol 60
report.

[toc] | [prev] | [next] | [standalone]

#1282 — Re: specifying semantics, was Formatting of Language LRMs

On 6/25/2014 9:54 PM, George Neuner wrote:

> Moreover, there are 3 broad categories of semantic description:
> operational, denotational and axiomatic.  Lambda calculus really is
> suitable only for expressing operational and/or denotational forms.
> Axiomatic descriptions generally take the form of a propositional
> algebra.

Where would you place VWG on the operational/denotational/axiomatic
spectrum?

[toc] | [prev] | [next] | [standalone]

#1284 — Re: specifying semantics, was Formatting of Language LRMs

On 28/06/14 20:25, Ivan Godard wrote:
> On 6/25/2014 9:54 PM, George Neuner wrote:
>> Moreover, there are 3 broad categories of semantic description:
>> operational, denotational and axiomatic. [...]
> Where would you place VWG on the operational/denotational/axiomatic
> spectrum?

	The point about vWGs is that they are *grammars*, so are not
themselves concerned with semantics.  What they do is push back the
boundaries between syntax and semantics, so that many concepts that
are usually thought of as semantic in nature are syntax in a vWG.
The canonical example is the relationship between declaration and
use of a given identifier;  in context-free grammars, this has to
be described outside the grammar, whereas in a vWG the declaration
can add the identifier and its type to a "nest" and each use can
check that the use is consistent with the current nest.

	As vWGs are Turing-complete, there is no difficulty *in
principle* in writing an entire compiler [or interpreter] as a vWG;
your source code would either fail to compile or would [entirely
from the grammar] generate machine code [or be interpreted].  In
such a case, there need be no "semantics" at all;  your program
either has a syntax error or else generates some output and reaches
a halt state.  The only *major* use of vWGs thus far stopped far
short of that;  the Algol 68 report broadly treats all compile-time
decisions and actions as syntax, and all run-time decisions and
actions as semantics.

	Actual Algol compilers stop far short even of that;  but
that is a QoI matter.  According to the Report, the code

	  ( int i; j := 2 )

is wrong simply because it does not correspond to any expansion of
the notion "program";  but I can't imagine any compiler would fail
to produce a helpful error message such as "j not declared" rather
than merely "syntax error".

--
Andy Walker,
Nottingham.

[toc] | [prev] | [next] | [standalone]

Page 1 of 3  [1] 2 3  Next page →

Back to top | Article view | comp.compilers

csiph-web