Defining Programming Languages

Recursivity of the Definition

Use of Abstract Syntax Tree

There are different styles of formal definition, using deduction rules for each syntactic construct which collectively define the semantics of program terms M, N etc, especially function definitions (lambda abstractions) fun(a)L (N'), in a data state s. As an example of comparison we use the rules defining function application (call) with call-by-value parameter passing.

For those semantics based on a deduction system (c.f. Post systems above), there are basically two dimensions of classification:

• What is the structure Rel of premises and conclusions?
• How does the conclusion depend on the premises?

	Rel structure	term semantics [[M]]	[[M]] =
rewrite steps	Term --> Term	Ground	{ N | M --> ... --> N and N irreducible }
complete rewrite	Term --> Ground	Ground	{ N | M --> N }
rewrite/valuation	(Term mix BaseVal) --> BaseVal	Generic BaseVal	{ X | M --> X }
valuation	(Term mix Value) --> Generic Value	Value	{ v | M --> v }
with state
rewrite steps	Term × State --> Term × State	State × (Ground × State)	{ (s, (N, s')) | (M,s) --> ... --> (N, s') and (N, s') irreducible }
complete rewrite	Term × State --> Ground × State	State × (Ground × State)	{ (s, (N,s')) | (M,s) --> (N,s') }
rewrite/valuation	Term × State --> (Generic BaseVal) × State	State × ((Generic BaseVal) × State)	{ (s, (X,s')) | (M,s) --> (X,s') }
valuation	Term × State --> Value × State	State × (Value × State)	{ (s, (v,s')) | (M,s) --> (v,s') }

where Term is a program term (a syntactic domain), Ground Term is an irreducible program term (a syntactic domain), Generic Ground is an irreducible generic program term (a syntactic domain), State is a mathematical environment and state model (a semantic domain), Value is a mathematical model of all values, including functions/generics (a semantic domain), and BaseVal Value is a mathematical model of non-generic values (a semantic domain).

1. Abstract Machine operational semantics: «tend to pull the syntax of [language] constructs appart and build non-intuitive auxiliary data structures» [OSPE].
2. Structural Operational Semantics (SOS), popularized by Plotkin (1981), is a syntax-directed approach for specifying the semantics of programs (which simplifies proofs by induction) [OSPE].
   1. Transition semantics = reduction semantics = small-step semantics (Plotkin's form of SOS) [OSPE].
      There are two kinds of derivation rules for the relation:

      • Rules that give the basic steps of reduction (axioms of the semantics' derivation system).
        E.g. (fun(x)L (v), s) --> (L, s[v/x])

        Rules for simplification steps that say how reductions are performed within a context. The latter can be more succinctly specified using the notion of evaluation context by Wright and Felleisen (1994).

        (M, s) --> (M', s') (M(N), s) --> (M'(N), s')

        (N, s) --> (N', s') (fun(x)L (N), s) --> (fun(x)L (N'), s')

      
      Based on them computation proceeds with the rewriting logic's deduction rules until an irreducible configuration is reached, i.e. one that cannot be rewritten any more.

      Evaluation semantics = big-step semantics = natural semantics (Kahn 1987) = relational semantics (Milner) [OSPE] has deduction rules of the following form:

      (M, s) --> (fun(a)L, s');   (N, s') --> (x, s'');   (L, s''[x/a]) --> (y, s''') (M(N), s) --> (y, s''')

3. In a denotational semantics deduction rules have the following form:

   (M, s) --> (f, s');   (N, s') --> (x, s'');   f(x) = y (M(N), s) --> (y, s'')

   The irreducible values are only single-token literal constants, or primitive values, respectively; function terms evaluate to mappings f. Treatment of recursion and loops requires least fixed points and domain theory. Category theory is used for modelling type systems. Rel (Term × State) × (NonTerm × State).
4. Axiomatic semantics TODO c.f. Hoare logic, Hoare triples

``In comparing the denotational semantics with the operational semantics, the denotational semantics does not seem to be much simpler. It may even be argued that it is a great deal more complex, because it requires an understanding of fixed points. The primary advantage of the denotational semantics is the intuitive explanation it provides [for OO inheritance]. It suggests that inheritance may be useful for other kinds of recursive structures, like types and functions in addition to classes. It reveals that inheritance, while a natural extension of existing mechanisms,, does provide expressive power not found in conventional languages by allowing more flexible use of the fixed point function.'' [William Cook, Jens Palsberg: A Denotational Semantics of Inheritance and its Correctness; 329-350 in: Information and Computing 114; 1994]

A state model for an OOPL has to relate

1. object-IDs plus field labels to values --- for modeling instance variables, aka object fields
2. local names (parameters, local variables, this) to values --- for modeling locals

		instance variables, aka object fields
		OID -> Id -> TermVal called (Object) Store [OT, Joe, CfS, Univ, Moby], or Store of Globals [J/Isa]	OID -> Id -> ValLoc + ValLoc -> TermVal
l o c a l s	Id -> TermVal called Stack Frame [OT], Bindings [Joe], or Store of Locals [J/Isa]	[J/Isa] State = Store-of-globals × Store-of-locals [JTS] State = OID->Id->Val Id->Val [JavaS] State = OID->HeapObj (Id->Val)* [Univ] State = {$} -> Store Id -> Val [CfS] Store = (Id (OID x Id) -> Val [OT] Store and Stack-frame* [Joe] Store and Bindings	[PolyTOIL] Store = Loc -> Irr and Environment = Id -> Irr where Loc =^= OID ValLoc, Irr =^= PrimVal Loc, PrimVal OID =^= TermVal, Env =^= Id -> TermVal (for parameters) Id -> ValLoc (for local variables) reachable Store =^= OID -> Id -> ValLoc ValLoc -> TermVal
	Id -> ValLoc + ValLoc -> TermVal
	substitution	[Moby] Object store (and evaluation context stack) [OOC] Store

Computing with Rewriting Systems

``To compute ... one performs equational simplicitation by using the equations from left to right until no more simpliciations are possible. Note that this can be done concurrently, i.e., applying several equations at once'' [

Rewriting logic [LTCO] is a logic for deducing how to rewrite terms based on a set of rewrite rules from a rewrite theory (see above) with the first four following deduction rules. Equational logic is obtained from rewriting logic by adding the symmetry rule.

1. Reflexivity:	M --> M
2. Congurence [c.f. eager evaluation]:	f(M1, ... Mn) --> f(N1, ... Nn)	if M1 --> N1 through Mn --> Nn
3. Replacement for each rewrite rule f(x1, ... xn) --> g(x1, ... xn):	f[M1/x1, ... Mn/xn] --> g[N1/x1, ... Nn/xn]	if M1 --> N1 through Mn --> Nn
4. Transitivity:	M --> N	if M --> L and L --> N
5. Symmetry:	M --> N	if N --> M

In rewrite logic, a sequent "M --> N" should be read "M becomes N". In equational logic, a sequent "M --> N" can be read "M equals N".
``[R]ewriting logic is a logic of becoming or change, not a logic of equality in the static Platonic sense. Adding the symmetry rule is a very strong restriction, namely assuming that all change is reversible, thus bringing us into a timeless Platonic realm in which "before" and "after" have been identified. [LTCO]

Classification

1. Syntactic rewriting:
   • Labelled transition systems (model concurrency as interleaving)
   • Functional programming ``corresponds to the case of confluent rules'':
     • Lambda calculus (in combinator form)
     • Herbrand-Gödel-Kleene theory of recursive functions
     • Algebraic datatypes (?)
       • Free datatypes
2. Rewriting modulo associativity and neutral elements (e.g. nil for lists):
   • Post systems
     • Phrase structure grammars, including:
       • Turing machines
3. Rewriting modulo associativity, commutativity, and neutral elements:
   • Petri nets
   • Chemical abstract machine [Berry and Boudol: The Chemical Abstract Machine; 91-94; POLP'90], specializes to:
     • CCS [Robin Milner: Communication and Concurrency; Prentice-Hall 1989]
   • Concurrent programming:
     • Unity's model of computation [K M Chandy, J Misra: Parallel Program Design: A Foundation; Addison-Wesley 1998]
     • Higher-level Petri nets for actors: POT and POP [Engelfriet: Net-based description of parallel object-based systems, or POTs and POPs; Technical Report, FOOL; 1990]

For a comprehensive overview over all the formal models developed for reasoning about object-oriented language semantics you must read:
Tom Mens: A survey on formal models for OO, 1994.

• The lambda-calculus (LC) expresses functions and function application. Cf. type system development (mostly based on LC)
• Object calculi are based exclusively on objects rather than functions (taken from here).
  • Martin Abadi and Luca Cardelli's Theory Of Objects is a typed object calculus. See also their sigma calculus in A Theory of Primitive Objects
  • Laurent Dami's HOP Calculus is a functional OO-calculus.
  • Kim Mens, Tom Mens, Patrick Steyaert and Kris De Volder's OPUS Calculus is an object-oriented programming calculus.
  • John C. Mitchell and Kathleen Fisher's delegation-based object calculus (work in progress).

Analysis

Requirements & Principles

Paradigms

Abstractions

Domains

Features

foundational

safety

flexible typing

Syntactics

Defining PLs

Language List