Gödel (programming language): Difference between revisions

Revision as of 17:45, 7 May 2013

Revision as of 17:46, 7 May 2013

Line 19:

}}

Gödel is a general-purpose, [[declarative programming language]] based on one of the four main programming paradigms, namely, [[logic programming]]. It was developed by Patricia M. Hill and John W. Lloyd. Basic ideas and features of Gödel are mainly taken from [[Prolog]] language. It is named in honour of logician [[Kurt Gödel]], although the acronym ‘God’s‘God's Own Declarative Language’Language' is sometimes used.

Gödel is a [[strongly typed]] system based on many-sorted logic with parametric polymorphism. It involves many data types and modules, supports integers and floating-point numbers of an arbitrary precision (including infinite precision. The Gödel language enables to solve constraint problems over finite domains of integers or rationals. It supports processing of finite sets. It offers a flexible computation rule and a pruning operator which generalises the commit of the concurrent logic programming languages. The declarative nature of Gödel programs makes Gödel well suited as a teaching language (because students can concentrate much more on writing down what it is they want to compute without being so concerned about how to compute it). Gödel narrows the gap between theory and practice in logic programming, since it reduces a significant number of non-logical features without useful semantics, and so Gödel language provides a bridge between theory and practice. Gödel’sGödel's meta-logical facilities provide significant support for meta-programs that do analysis, transformation, compilation, verification, debugging, and so on. Gödel’sGödel's meta-programs participate in building of some desirable applications: compiler-generators and declarative debuggers to debug Gödel programs (declarative debugging is an attractive debugging technique which only requires that the programmer know the intended interpretation of a program to locate certain bugs and, for example, knowledge of the procedural behaviour of the Gödel system is not needed). Gödel more easily allows a parallel implementation since there are only a couple of non-logical features to complicate matters.

Very detailed overview of Gödel programming language, precise descriptions and formal definitions of the syntax and semantics of the language with many examples and background material on logic can be found in the book <ref name=HillLloyd></ref>.

Line 33:

Currently in the Information (Computer or Digital) Age, programming languages are crucial communication tools to computers, mobile (smart) telephones and other devices. Programming languages can be divided into three dominant groups: general purpose programming languages, ___domain specific programming languages and modelling languages. Usage of a particular type of programming language depends on the project and knowledge of particular languages. The initial point of the programming process is the understanding of a particular problem that a programmer is trying to solve. The problem is then formalised as an intended interpretation of a language which in case of Gödel is a first-order language. The intended interpretation specifies the various domains and the meaning of the symbols of the language in these domains.

The first-order language (as Gödel’sGödel's intended interpretation) is, roughly speaking, a specific model of computation arising from logic programming paradigm, which is one of the four main paradigms, i.e. fundamental style of computing programming. Other paradigms are [[object-oriented]], imperative and functional (with concrete models of computation, particularly, [[Turing machine]] for object-oriented and imperative programming, λ-calculus for functional [[programming paradigm]]. The [[first-order logic]], sometimes called as first-order predicate calculus, the lower predicate calculus, quantification theory, and less precise as predicate logic, is a formal system used in mathematics, philosophy, linguistics and computer science. Unlike propositional logic the first-order logic uses quantified variables. The first-order logic satisfies several meta-logical theorems that make it open to analysis in proof theory. It is the standard formal logic for axiomatic systems; hence it plays an important role in the [[foundations of mathematics]]. Many common axiomatic systems, such as first-order Peano arithmetic and axiomatic set theory, including the canonical [[Zermelo-Frankel set theory]], can be formalised as first-order theories.

Obviously, [[higher-order logic]] exists where, typically, predicates have other predicates or functions as arguments, or in which one or both of predicate quantifiers or function quantifiers are permitted. In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets. No first-order theory, however, can fully and categorically describe structures with an infinite ___domain, such as the natural numbers or the real numbers. Categorical axiom systems for these structures can be obtained in stronger logic such as second-order logic.

Line 43:

Declarative programming in general can be understood in a weak and a strong sense. In the weak sense, declarative programming means that programs are theories, but that a programmer may have to supply control information to produce an efficient program. Declarative programming, in the strong sense, means that programs are theories and all control information is supplied automatically by the system. In other words, for declarative programming in the strong sense, the programmer only has to provide the intended interpretation (or, perhaps, a theory which has the intended interpretation as a model). Gödel itself is a contribution to declarative programming in the weak sense. Thus Gödel programs are theories, but programmers are largely responsible for providing suitable control information.

Declarative programming is much more concerned with expressing the logic of a computation without describing its control, i.e. describing what the program should do, rather than describing how (that is the control part) it should be computed. Logical sentences can also be understood procedurally as goal-reduction procedures (also known as routines, subroutines, methods, or functions) with well set series of computational steps to be carried out. The Gödel programming language is not a procedural language. Although, the main advantage of the procedural semantics is portability, so that one could port a program from one implementation to another and be confident of identical behaviour of the program in the two systems, Gödel’sGödel's procedural open semantics gives more freedom to handle it by programmers and adapt resulting programs to special project requirements; the programmer can use the known behaviour of the program executor to develop a procedural understanding of his program. This may be helpful when seeking better execution speed.

[[Prolog]], [[HTML]], [[SQL]] together with Gödel rank among [[declarative programming languages]], while [[C/C++]], [[Fortran]] and [[Pascal]] are examples of [[procedural programming languages]].

Line 58:

[[Parametric polymorphism]] is the second most important aspect of the type system. It is common for programmer to want to write a definition of a predicate for which the arguments of the predicate vary in used types. For example, the Append predicate is normally written so that it can append lists of any type. A symbol is polymorphic if its declaration contains a parameter; otherwise it is monomorphic. A polymorphic symbol can be understood as representing a collection of (monomorphic) symbols.

Gödel’sGödel's type system is a strongly typed system. It means that each constant, function, proposition, and predicate in a program and its type must be specified by a language declaration. In particular, strongly typed nature of the Gödel programming language gives specific restrictions on permitted operations involving values of different data types, preventing the compiling errors or running of source code which uses data in an invalid way. By contrast, variables have their types derived from their context.

=== Modules ===

A module system simply provides a way of writing large programs so that various pieces of the program don’tdon't interfere with one another because of name clashes and also provides a way of hiding implementation details. The Gödel module system is based on these standard ideas. A Gödel program is a collection of modules. A module generally consists of two parts, the export and the local part. The export part of a module consists of language declarations for the symbols available for use in either part of the module and in the other modules which import them, control declarations, and module declarations giving the symbols from other modules which are available for use in either part of the module and in other modules which import them. The local part of a module consists of language declarations for the symbols available for use only in this part, module declarations giving the symbols from the other modules available for use in this part, control declarations, and definitions of those propositions and predicates specified by language declarations in this module.

The Gödel language include modules that process numbers, lists, strings and sets, modules that provide input/output, and modules that provide meta-programming facilities. Gödel also makes significant use of abstract data types, which are implemented by means of the module and type systems. An abstract data type consists of a type and a collection of operations on the type. Abstract data types have many advantages for software engineering, including the provision of a higher level of abstraction for programmers and the ability to change the implementation of a type without affecting existing code. The Gödel system modules provide a number of important abstract data types, including Unit (the type of units which are term-like structures), Flock (the type of ordered collections of units), Program (the type of terms representing Gödel programs), and Theory (the type of terms representing polymorphic many-sorted first order theories). The corresponding module provides a collection of operations on the type and the module system is used to hide the implementation details of these operations. Furthermore, a number of other Gödel system modules provide types which are at least partly abstract.

Line 75:

Gödel has constraint-solving capabilities in the domains of integers and rational numbers. It can solve systems of (not necessarily linear) constraints which involve integers, variables which range over bounded intervals of integers, and the usual functions and predicates with integer arguments. It can also solve systems of linear rational constraints involving rationals, variables ranging over the rationals, and the usual functions and predicates with rational arguments.

The Gödel pruning operator (a difference from Prolog’sProlog's pruning operator is shortly explained below), called the commit, can be used to prune away parts of a search tree and can thus affect the completeness of the search procedure. The commit is a powerful pruning operator and, in its full generality, is primarily meant to use by source-levels tools, such as partial evaluators and program transformers. Thus Gödel provides two special cases of the commit with simplified notation for use by programmers. These are the one-solution commit and the bar commit. The one-solution commit prunes the search tree in such a way as to ensure (at most) one solution of the formula it contains will be found. The bar commit which is similar to the commit of the concurrent logic programming languages, provides a means of pruning some of the branches emanating from a node in a search tree, where each branch corresponds to a statement in the program whose head unified with the selected atom in the goal labelling that node. However, while commits are infrequently needed in Gödel programs because their effect can often be achieved with declarative constructs such as negation and if-then-else, their use does detract from the major aim of Gödel, which is to have programs with the best possible declarative semantics. However, (sound) pruning operators do have an important place in logic programming languages, even though they may adversely affect the semantics of programs in which they appear.

The other facility provided by Gödel that gives a form of control is the IF-THEN-ELSE construct, which has several variations. This construct has a declarative meaning, but also provides the important control information that the condition in the IF part should be computed only once. This can result in an important saving if this condition is computationally expensive. One variation omits the ELSE part and another allows existentially quantified variables to appear in the IF and THEN parts. The IF-THEN-ELSE facility figures prominently in the Gödel programming style.

Line 85:

=== Input/Output ===

Unfortunately, at the interface between a program and the external world, the declarative semantics of a program can be severely compromised. To try to ameliorate such difficulties, it is recommended that programmers exploit Gödel’sGödel's module system. The idea is to have all the modules which use [[input/output]] predicates as high as possible in the module hierarchy. This means that modules not above or equal to these input/output modules will not make any calls to input/output predicates. Thus they will contain pure code together possibly with commits.

Input/output and pruning facilities adversely affect the declarative semantics of Gödel programs. Input/output introduces side-effects via read predicates. However, this problem can be ameliorated by appropriate use of the module system. Commit affects the declarative semantics because it can cause correct answers to be pruned. Fortunately, Gödel programs generally need few uses of pruning. Except where use is made of either of these two facilities, Gödel programs are declarative.

Line 96:

In general, any programming language should satisfy five properties. It should be: high level (providing concepts as close as possible to those which people like to use to express their thoughts and ideas), expressive (providing concepts that can be used to model real-world situations easily and concisely), efficient (programs run at speeds and memory costs similar to competing languages), practical (that can be used for large-scale, real-world applications), and of a simple (mathematical) semantics (for which programmers can relatively easily verify and debug their programs and be assured of the correctness of program transformations, optimalisations, and so on).

Prolog is high level, efficient and practical. However, it is not sufficiently expressive as the logic it uses is untyped. Then, Prolog’sProlog's semantics is not satisfactory, for example, provides a little of check, uses unsafe negation and cut, uses non-logical predicates, such as var, nonvar, assert, and retract. These problematical aspects of Prolog cause many practical Prolog programs to have no declarative semantics at all and to have unnecessarily complicated procedural semantics. This means that the analysis, transformation, optimisation, verification, and debugging of many Prolog programs is extremely difficult.

The solution to these semantic problems it to take more seriously the central thesis of logic programming, which is that

Line 105:

Gödel directly addresses these semantics problems of Prolog. The main design aim of Gödel is to have functionality and expressiveness similar to Prolog, but to have greatly improved declarative semantics compared with Prolog. Gödel is intended to have the same relation to Prolog as Pascal does to Fortran. Prolog was designed at the birth of logic programming before researchers had a clear understanding of how best to handle many facilities. Consequently, these facilities compromised its declarative semantics.

Prolog’sProlog's approach to meta-programming is one of its most unsatisfactory aspects. Prolog does not make a clear distinction between the object level and meta-level, and does not provide explicit language facilities for representation of object level expression at the meta-level. Thus important representation (that is, naming) and semantics issues are glossed over. Prolog’sProlog's meta-programming problems can be traced to the fact that it does not handle the representation requirements properly. A consequence of this is that it is not possible to understand most Prolog meta-programs as theories and hence they do not have a declarative semantics. The most obvious symptom of this is with var, which has no declarative semantics at all in Prolog. However, within the framework of the appropriate representation, a meta-program is a first order theory and the meta-logical predicates of Prolog, such as var, nonvar, assert and retract, have declarative counterparts.

Example of meta-program: the standard solve interpreter. This interpreter consists of the following definition for solve.

Line 136:

Prolog uses the cut as its pruning operator. However, cut has a number of semantic problems. The first of these problems is that cut, at least as it is employed in existing Prolog systems, allows considerable uncertainty about what the underlying logic component of the program is. This is because programmers can exploit the sequential nature of cut to leave “tests” out and when this is done the logic component of the program cannot be obtained by simply removing all the cuts from the program. Furthermore, there is no convention for systematically putting back the omitted tests so as to define the logic component precisely. The second problem with cut is that its use, in the presence of negation, can be unsound, in the sense that a computed answer may not be correct with respect to the completion of the logic component of the program.

For these reasons and because the commit of the concurrent logic programming languages has better semantics, Gödel’sGödel's pruning operator, also called commit, is based on the commit of the [[concurrent language]]s. In fact, the simplest form of the commit (denoted | and called bar commit) is similar to the commit of the concurrent languages. Consider the following definition of the proposition M, in which we write | as a connective with the declarative meaning of conjunction.

M <- Q | R.

Line 214:

Gödel programming language benefits from previous designed languages and work of many authors. It is based on, and supposed to be a successor of Prolog that was developed by Alain Colmerauer in 1972. Gödel then contains:

* the intensional set terms developed from set processing facilities introduced around 1980 into Prolog by David H.D. Warren

* pruning operator first appeared in the Relational Language of Keith Clark and Steve Gregory in the early 1980’s1980's

* the if-then-else construct and the when control declaration taken from NU-Prolog introduced by Lee Naish around 1986

* the type system based on many-sorted first order logic with the addition of polymorphism through parameters and constructors

* the ideas of the polymorphic component are made by Robin Milner (introduced in ML in the 1970’s1970's) and are first considered in the logic programming context by Alan Mycroft and Richard O’KeefeO'Keefe in 1983

* the module system is based on standard ideas of Modula-2

* the constraint solving facilities are partially developed by Alain Colmerauer, Joxan Jaffar, Jean-Luis Lassez (influenced by work of Kenneth Bowen and Robert Kowalski which itself relies on work of Kurt Gödel)