13 Oct 2002 16:00:24 -0400

Related articles |
---|

[4 earlier articles] |

Re: Formal semantics of language semantics joachim_d@gmx.de (Joachim Durchholz) (2002-09-29) |

Re: Formal semantics of language semantics stephen@dino.dnsalias.com (Stephen J. Bevan) (2002-09-29) |

Re: Formal semantics of language semantics lex@cc.gatech.edu (Lex Spoon) (2002-09-29) |

Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-09-29) |

Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-13) |

Re: Formal semantics of language semantics haberg@matematik.su.se (Hans Aberg) (2002-10-13) |

Re: Formal semantics of language semantics scgupta@solomons.cs.uwm.edu (Satish C. Gupta) (2002-10-13) |

Re: Formal semantics of language semantics lex@cc.gatech.edu (Lex Spoon) (2002-10-13) |

Re: Formal semantics of language semantics anw@merlot.uucp (Dr A. N. Walker) (2002-10-18) |

Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-10-18) |

Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-10-18) |

Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-20) |

Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-20) |

[6 later articles] |

From: | "Satish C. Gupta" <scgupta@solomons.cs.uwm.edu> |

Newsgroups: | comp.compilers |

Date: | 13 Oct 2002 16:00:24 -0400 |

Organization: | Compilers Central |

References: | 02-09-149 02-09-169 |

Keywords: | semantics |

Posted-Date: | 13 Oct 2002 16:00:24 EDT |

*> I found Benjamin Pierce's new book "Types and Programming Languages"*

*> be an excellent introduction to specifying and using semantics, as*

*> well as on types. It's aimed at a fairly low reading level, so that*

*> you don't need a math degree to understand it.*

I agree, Benjamin Pierce's book is really good. I took a course on

Type Theory and the instructure used a draft of the book. It was

pretty smooth. However I don't agree that the material is trivial.

True that you don't need a math degree but should know basic set

theory and logic (proof by induction, proof by contradiction etc.).

Basically, you should know discreet math. That is the only prereq to

understand the book.

*> I have no idea how well the methods in the book scale to larger, more*

*> complicated programming languages. In industry, everyone seems to use*

*> natural language most of the time. Then, if they really want a formal*

*> sematics, then they may write one up in a theorem prover such as HOL.*

*> These after-the-fact semantics are almost certainly horrendous to*

*> read, though I admit I haven't even bothered to try. It's interesting*

*> to consider what it wold be like if languages were formally specified*

*> from the beginning.*

These methods have been used to define most part of Java (and some

problems in its type system were discovered in the process). If you

are interested you can take a look of a paper in ACM's TOPLAS:

http://portal.acm.org/citation.cfm?doid=503502.503505

or http://www.cis.upenn.edu/~bcpierce/papers/fj-tr.ps

This paper is by Atsushi Igarashi, Benjamin Pierce, Philip Wadler.

There are papers from other authors as well, some of them are:

http://research.microsoft.com/~dsyme/reports/java.ps

http://www-sop.inria.fr/oasis/personnel/Marjorie.Russo/java/

There are more, but I have to dig.

I think nobody in the industry uses formal semantics because of two

reasons:

1. most of the formal semantics papers/books start with defining

a notation and then build a type system framework on top of it.

So, unlike BNF, there are multiple notations out there, and a

symbol in two notations might mean two different things. notations

are converging but still there are gaps. I think that over time,

some notation might become a de facto standard notation to describe

type systems. Perhaps, someone will write a handbook to use for

reading and defining type systems.

2. formal semantics is not as easy as formal syntax, simply because

semantic rules are much more complex than syntax rules. It is very

hard to read and understand formal semantics of a non trivial

language. If you look at complete set of formal semantics rules

for a language with basic OO features (inheritence, method

overloading and overriding), I bet anybody would be scared. It

takes time, effort and persistence to become confortable with it.

Once you are confortable, you might happen to like it because these

rules are very precise. I think that is why people settled for

ambiguous prose describing semantic rules.

+satish

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.