© Jørgen Steensgaard-Madsen, Copenhagen, 2006
Implicit vs. explicit introduction of names                                                  
 
   

A mathematical characterisation of programming languages must describe meanings of names. One approach is to use techniques also known from compiler construction: name tables can map names into their meanings. Mathematically this is fine, provided the meanings are proper mathematical entities. Unfortunately this has an inherent fundamental problem: computations are not well-known, mathematical entities.
Denotational semantics purports to characterise languages in a framework of first-order functions (i.e. functions with domain and ranges that do not contain functions). This makes it hard to describe programs that use higher-order functions (even the simple case where a function's domain may contain functions). Furhtermore, such characterisations assumes existence of primitives that are hard to distinguish from what has to be described (e.g. branching and memory).
Methods of abstract algebra focuses on expressions as mathematical entities, and in this sense comes close to computations. However, abstract algebra is typically also restricted to first-order entities, and shares in this respect problems with denotational semantics.
Operational semantics describe computations by transformation rules similar to proof rules of formal logic. Inherently this is close to the notion of computations. There is a strong relationship between proofs and programs, which is known colloquially as `the proposition as types analogy' or `the Curry-Howard isomorphism'. However, higher-order logics are considered a little exotic and its relationship with programming may not be worked out.
The Howard languages rely critically on the notion of higher-order computations, i.e. computations that rely on abstract, named computations. However, computations that return computations (as in ML, for example) have been left out by design for various reasons.
The is_file operation is a simple example of a higher-order computation of practical interest: its second clause is a computation that depends on names that characterise file attributes. Usually the computation will be extremely simple, consisting of just one of the names; but the principles involved cover much more complex examples.
An application of is_file shown earlier is: is_file("/home",absent). Without implicit introduction of names, the signature of is_file would lead to an equivalent expression like
is_file(¯ is_file("/home",
  l(link,absent,directory,regular,socket,fifo,other)absent)
Not only is this substantially longer, it is also harder to use because not only the meanings of the various values must be remembered, but their sequence as well. Should the signature be changed, e.g. by addition of attribute characteristics, the expression would have to be changed as well. Implicit introduction of names will be unaffected even by deletion of attribute characteristics other than the ones actually used.
Implicit introduction of names is used for operator symbols in Howard languages. Explicit introduction of them would lead to substantial problems about determination of attributes like precedence and associativity, as well as about overloading.
The more complex variant of an application of is_file disregard details of types. Introduction of type names would add to the complexity, if explicit introduction is used and lead to notational and semantic problems that are easily solved when explicit introduction is used, as an example may illustrate. Consider
var x{ x:=0; var y{ y:="checking"; ....}}
The var-operation introduces a type lvalue and uses it to identify the meaning of an := operator where it is used. With explicit naming other means seems to be required. Note in passing that the example illustrates that the chosen type name lvalue has to be combined with a nesting level to be unique, and that uniqueness is required to ensure correct type checking.
For the benefit of users who are not convinced by the discussion above, dulce does support a syntax that allows renaming of ordinary operation names (i.e. neither type names nor operator symbols nor operations of special significance: __ and _). The is_file example may be expressed as
is_file("/home")\(l,a,d,r,s,f,o)(a)
i.e. with l represented by a back-slash. This kind of renaming is allowed wherever a label is.

Contents

Demo language
·Implementation tool
Copyrights


Introduction
·Principles
Interpreter construction


Deep- and surface structures
Design issues
Abstract type operatorss
Description of operator
·Name introduction
Data abstraction and control



File translated from TEX by TTH, version 3.33.
On 18 Oct 2006, 16:47.
SourceForge.net Logo