Algebraic Design Language
Richard B. Kieburtz, Lewis Jeffrey · 1994
This report constitutes a preliminary definition of a new, high-level programming language called ADL. It uses the mathematical concept of structure algebra as this unit of modularity. When algebra''s are used to specify programs, control structure is fixed first and data structures, or representations, second. There is no explicit recursion or iteration construct in ADL. Control is determined by combinators applied to inductively defined algebra''s. An intended use of ADL is to provide computational semantics of specialized software design languages. An algebra in ADL can be interpreted in carious monads, a particular variety of algebras that has been found useful in programming. ADL also makes use of coalgebras, a concept dual to that of algebras. With coalgebras, iterative control structures typical of search algorithms can be specified. There is a strong notion of type in ADL, guaranteeing that all well-typed programs terminate. This allows us to use sets as ADL''s semantic domain and to provide ADL with an equational logic. However, to check the type correctness of an expression, there can be proof obligations that cannot be discharged mechanically. A benefit of the equational logic is that an ADL program is amenable to transformation based upon the equational logic that an ADL program is amenable to transformation based upon the equational theories of its algebras. Transformations are not discussed in this report, however.