Three-dimensional visual language for higher-order logic 

Three-dimensional visual language for higher-order logic.

Related languages
Enhanced Show-and-Tell => CUBE   Extension of

  • Najork, M.A., Kaplan, S.M. "The CUBE Language" view details
          in Proc. of the 1991 IEEE Workshop on Visual Languages, Kobe, Japan, October 1991 view details
  • Najork, M. A. and Kaplan S. M. "A Prototype Implementation of the CUBE Language" view details
          in Proc 1992 IEEE Workshop on Visual Languages, Seattle, Washington, September 1992 view details
  • Najork, Marc A. "Programming in Three Dimensions" Journal of Visual Languages & Computing 7(2) June 1996, pp219-242 view details Abstract: Cube is a three-dimensional, visual, statically typed, higher-order logic programming language, designed to be used in a virtual-reality-based programming environment. In this paper, we give an informal overview of the language and describe a prototype implementation.
    DOI Extract: The Cube Language
    The Cube Language
    Semantically, Cube is a logic programming language, similar to Prolog. Prolog, however, is a first-order language, while Cube is higher-order, meaning that predicates are first-class values and can be passed as arguments to other predicates. The expressive power of higher-order languages is well-known. Higher-order features are standard in functional languages and have been incorporated into a few (textual) logic languages as well, such as lProlog and HiLog.
    A second difference between Prolog and Cube is that Prolog is an untyped language, whereas Cube has a static polymorphic type system. The Cube system uses a variant of the Hindley-Milner type inference algorithm to ensure that programs are well-typed; such well-typed programs are guaranteed to never encounter a run-time type error.
    Extract: Introduction
    This paper describes Cube, the first visual language to employ a three-dimensional (3D) notation. Apart from its novel syntax, Cube is innovative in other aspects : it is the first visual language to apply the dataflow paradigm to logic programming; it is among the first visual languages with a static polymorphic type system, and guarantees the absence of run-time type errors; and it is a higher-order language, meaning that it treats predicates as first-class values. The main part of the paper elaborates on these innovations. At this point, however, we would like to motivate Cube?s most obvious innovation, the use of a 3D syntax.
    Extract: The Dataflow Metaphor
    The Dataflow Metaphor
    Consider the simple program shown in Figure 1. It consists of two transparent cubes that are connected by a pipe. The transparent cubes are called holder cubes; they may contain terms (which are represented by cubes as well), and thus correspond quite closely to variables in a textual language.
    The left holder cube contains a term : an opaque cube with the icon ?1? on its top side. This cube is called an integer cube, and represents the integer 1. The two holder cubes are connected by a pipe which serves as a ?conduit? for values. The metaphor we use here is the dataflow metaphor : during evaluation, a value contained in a holder cube flows to all the other holder cubes connected to it. If a holder cube receiving a value is empty, it will be filled with this value, if it already contains a value, the two values must be unifiable; both holder cubes will then contain the same value, namely, the most general unifier of the two values. If this is not possible, the dataflow fails.
    Pipes have no particular directionality : data can flow through them in either direction, in fact it can flow in both directions at once. It should also be noted that the value contained in a holder cube never gets changed but only refined. We can extend the analogy we have drawn between Cube and textual languages : Holder cubes correspond to logic variables, and connecting two holder cubes by a pipe corresponds to unifying two logic variables. Furthermore, a holder cube containing a term cube (such as an integer cube) corresponds to a logic variable unified with a term.
    In the textual framework, a unification is a special case of an atomic formula. A Cube program (i. e. the entire ?virtual space? in which Cube expressions are located) corresponds to a query in a textual logic language, that is, a conjunction of all the atomic formulas.
    Figure 2 shows the Cube program of Figure 1 after evaluation. The integer cube 1 has flown from the left to the right holder cube (intuitive interpretation); or the left holder cube was unified with 1 and with the right one, leaving both instantiated to 1 (logic interpretation).
    Some Cube queries do not have any solutions. For example, if the right holder cube in Figure 1 contained a value other than 1, say 2, the dataflow between the two holder cubes would fail because 1 and 2 are not unifiable, thereby causing the entire computation to fail.
    Extract: A First Glimpse at Types
    A First Glimpse at Types
    We have mentioned before that Cube is a statically typed language and uses a type inference system. The user can trigger the type inference; the Cube system will then determine if the program is well-typed and, if so, will indicate the type of every empty holder cube by placing a type cube inside it. A type cube is an opaque grey cube with an icon on its top that identifies the type. There are three predefined base types : integers, floating-point numbers and propositions. Cube also allows the user to define new types, such as characters, strings, lists, or trees.
    Given the program from Figure 1, Cube will infer that 1 is an integer, so the left holder cube contains an integer, and therefore the right holder cube must contain an integer as well. It will thus fill the right holder cube with a type cube with the icon ?Z? on its top, representing the integer type (see Figure 3).
    What happens if Cube cannot determine the type of a holder cube? In other words, how do we represent uninstantiated type variables? An uninstantiated type variable is shown as a grey type cube with a unique index in the northwest corner of its top side.
    The same concept is used for uninstantiated variables : a variable of type  t is shown as t ?s type cube with a unique index in the southeast corner of its top side; the cube is green because it represents a value. (Figure 17, appearing in a subsequent section, gives an example of uninstantiated variables and uninstantiated type variables. )
    Extract: Predicate Applications
    Predicate Applications
    A predicate cube is represented by an opaque green cube with an icon on its top that identifies the predicate. A predicate cube typically also has a number of ?holes? in its sides : cubic intrusions with a transparent cover on the outside and an icon on top of it. The ?holes? are called ports and serve as arguments to the predicate. They may be moved around freely over all six sides of the predicate cube; thus, an icon is needed to identify each port. A port is a special case of a holder cube (hence the transparent cover), and as such it can be connected to pipes and can be filled with a value.
    So how can we apply predicate cubes? Assume we want to build a program to convert temperatures between the Celsius and Fahrenheit scale, which are related by the formula F 5 1 ? 8 C 1 32. The program shown in Figure 4 is the Cube representation of this relation. It consists of two empty holder cubes (corresponding to C and F ) and two holder cubes filled with floating-point values 1 ? 8 and 32 ? 0, respectively. It also contains a predicate cube referring to the floating-point multiplication predicate, and another predicate cube referring to the floating-point addition predicate. Both predicate cubes have three ports each, since in a logic programming context, addition and multiplication are viewed as ternary predicates. The first port of the multiplication predicate is connected by a pipe to the leftmost empty holder cube, the second one is connected to the holder cube containing the value 1 ? 8, and the third one (the ?result?) is connected to the first port of the addition predicate. Thus, if the user puts a value into the leftmost holder cube, the multiplication predicate will receive this value, will multiply it by 1 ? 8, and transfer the result to the addition predicate, which then adds 32 ? 0 to it, and transfers the result to the rightmost holder cube.
    Alternatively, if the user puts a value into the rightmost holder cube, it will flow into the ?result? port of the addition predicate cube, which will now subtract 32 ? 0 from it, and transfer the result of this subtraction to the ?result? port of the multiplication predicate cube. This cube will divide the result of the subtraction by 1 ? 8, and transfer the result of this division to the left holder cube.
    This example demonstrates that arithmetic predicates work in either direction. Addition, for instance, can use the first two arguments to produce the third one, or the last two to produce the first one. The ?multidirectionality? of predicate applications complements the bidirectionality of dataflow in Cube.
    In general, the addition predicate needs to know at least two values to determine the third one; otherwise, evaluation of the predicate is suspended until suf ficient information is available. There are Cube programs which cannot be ?solved? because not enough information is available. The temperature conversion program, with neither a Celsius- nor a Fahrenheit-value supplied to it, is such a program. If we try to evaluate it, the system reports that it is unable to decide whether the query is satisfiable or not.
    Extract: Predicate Definitions
    Predicate Definitions
    Cube also allows us to define new predicates, thereby providing a mechanism for ?procedural abstraction?. Moreover, these predicates may be recursive (that is, they may refer to themselves), which allows us to describe potentially unbounded computations.
    Assume we want to define a predicate that generates all the natural numbers, i. e. the integers greater than or equal to 1. The natural numbers can be recursively defined as follows : (a) 1 is a natural number, and (b) if n is a natural number, then so is n 11.

          in Proc 1992 IEEE Workshop on Visual Languages, Seattle, Washington, September 1992 view details