CmSc 315 Programming Languages

Chapter 4: Formal properties of Languages
Formal Models of Language Semantics

Learning goals

  1. Introduction

    The need for language semantics:

      1. for the programmer - to know how to use language constructs
      2. for the implementor - to know how to implement the language

    Informal descriptions of language semantics - provided in verbal form in the language manuals.
    May be ambiguous.

    Formal description of language semantics - studied theoretically,
    no satisfactory models have been produced so far.

  2. Semantic models

    • Grammatical models: grammar rules are paired with semantic rules.

    Resulting grammars are called attribute grammars

    See fig.4.3. and the example below, p.129

     

    Rule

    Attribute

    E ® E + T

    value(E1) = value(E2) + value(T)

    E ® T

    value(E) = value(T)

    T ® T x P

    value(T1) = value(T2) x value(P)

    T ® P

    value(T) = value(P)

    P ® I

    value(P) = value of number I

    P ® (E)

    value(P) = value(E)

     

    • Operational models

    Describe the meaning of the language constructs in terms of machine states,
    i.e. memory and register contents

    • Applicative models

    Treat programs as functions.
    Two methods to build applicative models:

    denotational semantics and functional semantics.

    Denotational semantics

    A technique for describing the meaning of programs in terms of mathematical functions on programs and program components. Programs are translated into functions about which properties can be proved using the standard mathematical theory of functions. Based on Lambda calculus.

    Lambda calculus

    Lambda calculus is a formal mathematical system devised by Alonzo Church to investigate functions, function application and recursion. It has provided the basis for developing functional programming languages. Lambda calculus also provides the meta-language for formal definitions in denotational semantics. It has a good claim to be the prototype programming language. More about lambda calculus: http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Ch/

    An example illustrating lambda calculus:

    (Author: Jim Larson, source http://www.jetcafe.org/~jim/lambda.html)

    A function accepts input and produces an output. Suppose we have a "chocolate-covering" function that produces the following outputs for the corresponding inputs:

    	peanuts	->	chocolate-covered peanuts
	rasins	->	chocolate-covered rasins
	ants	->	chocolate-covered ants

    We can use Lambda-calculus to describe such a function:

    	Lx.chocolate-covered x

    This is called a lambda-expression. (Here the "L" is supposed to be a lowercase Greek "lambda" character).

    If we want to apply the function to an argument, we use the following syntax:

    	(Lx.chocolate-covered x)peanuts -> chocolate-covered peanuts

    Functions can also be the result of applying a lambda-expression, as with this "covering function maker":

    	Ly.Lx.y-covered x

    We can use this to create a caramel-covering function:

    	(Ly.Lx.y-covered x)caramel -> Lx.caramel-covered x

    Functions can also be the inputs to other functions, as with this "apply-to-ants" function:

    	Lf.(f)ants

    We can feed the chocolate-covering function to the "apply-to-ants" function:

    	(Lf.(f)ants)Lx.chocolate-covered x
	-> (Lx.chocolate-covered x)ants
	-> chocolate-covered ants
    • Axiomatic models

    Describe the meaning as pre-conditions and post-conditions.
    Used in program verifications (see p.140)

    • Specification models

    Describe the relationship among various functions that implement a program.

    Example of a specification model:
    Algebraic data types - describe the meaning in terms of algebraic operations, e.g. pop(push(S,x)) = S

  3. Summary

    Formal models of syntax, grammars and parsing are well studied and widely used in programming language definition and implementation. Formal syntax definition can be used to construct parsers automatically from the definition.

    Formal models of semantics of programming language are not so successful. A lot of research is going on towards building semantics-directed compilers that would translate programs into machine language using a formal specification of the semantics of the programming language.

    Attribute grammars, that associate with each non-terminal in the grammar a set of attributes, are one of the earliest semantic models (Knuth, Donald E., Semantics of context-free languages, Mathematical Systems Theory 2 2 :127-145, 1968.) and they are still in use. Their most beneficial feature is that they can be used for efficient automatic translation. However, attribute grammars are not sufficiently powerful to represent the entire semantics of programming languages - they are too tightly coupled with parse trees.

    A very powerful formal model, that can represent any computable function, is the denotational semantics (Scott, D.S. and Strachey, C., Towards a mathematical semantics for computer languages, in Proc. Symp. Computers and Automata , pages 19-46. Polytechnic Press, NY, 1971.) However its practical application is quite complex .

Learning goals
  • Acquire the general idea about semantic models.

Back to contents
Created by Lydia Sinapova