jha@cs.ed.ac.uk (Jamie Andrews) (02/18/91)
>From: turpin@cs.utexas.edu (Russell Turpin) >Summary: What is the point of such obfuscation? >It takes greater mathematical sophistication to understand >infinite data structures. I can explain a circular queue to >the average sophomore taking a Pascal class in about three >minutes. To explain its equivalence as an infinite data >structures, I have to either talk about the view of the finite >structure as its pointers are infinitely chased, or I have to >talk about taking quotients, ie, mapping the infinite structure >onto the finite structure. What is the point? What is the >advantage of considering something that is essentially finite >as an infinite expansion? Oh, yeah. So you can program it >in Prolog. [Sorry for the long quote -- I thought it was necessary to get the impact of Russell's criticism.] I think there are several reasons for your feeling, which might not be the whole story, but which in any case you haven't mentioned. o In Pascal, looping data structures are seldom printed out as single entities because that's not usually the point of using them. Prolog is an interactive language in which some attempt at this must be made. If you try to print out such data structures in Pascal, the results are just as confusing. o Manipulations of such data structures are greatly facilitated by languages with explicit types, named record fields, and so on. Pascal has these; most Prologs don't. o You're taking an "operational" view of these structures, which may well be appropriate for some tasks, or for showing how the structures are implemented on the machine and why we want to use them. For other tasks, it may be appropriate to view the "pointed-to" nodes as part of the same structure as the records. In a nice LP language with a reasonable syntax, it should be possible to write very clear code which handles recursive data structures in a logical way, whether they're looping or not. In fact, the code might be nicer than Pascal because the dereferencing operation is not needed. It may still be advantageous to know about the pointer view to see how programs work; but, as in many things, the logical view may be better for certain problems. And here's an idea for the printout problem: perhaps in the declaration of data structures, the user could specify which nodes are to be printed along with the top-level structures, and which are to be printed as pointers, to be displayed further at the user's discretion. --Jamie. jha@cs.ed.ac.uk "Where in New York will I bury my twenties?"
markh@csd4.csd.uwm.edu (Mark William Hopkins) (02/24/91)
In article <6406@skye.cs.ed.ac.uk> jha@lfcs.ed.ac.uk (Jamie Andrews) writes: >o Manipulations of such data structures are greatly facilitated > by languages with explicit types, named record fields, and so > on. Pascal has these; most Prologs don't. Predicates ARE records only in disguise... PASCAL: type Complex = record RE, IM: real end; PROLOG: complex(RE, IM) :- real(RE), real(IM). if floating point came with your Prolog complete with its own real() predicate. Or better yet as an example: PASCAL: type NodeTag = (RE, INT); Node = record case Tag:NodeTag of RE: (RVal: real); INT: (IVal: integer) end PROLOG: node(RE, X) :- !, real(X). node(INT, X) :- !, integer(X). Prolog types are far more powerful than corresponding Pascal types, furthermore, since types in "procedure call"-s can be matched by Unification in Prolog. The closest thing you have in Pascal is the limited Polymorphism that the Standard attempted with array types. A similar argument also proves that Prolog is a very powerful object-oriented language in disguise. Also, if you consult the lambda calculus and functional programming literature, you'll find out about results concerning the correspondence (isomorphism) between types and propositions which underlies this observation (records <-> AND, unions/variants <-> OR, functions <-> IMPLICATION, etc.)
jha@cs.ed.ac.uk (Jamie Andrews) (02/28/91)
In article <9732@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: >Predicates ARE records only in disguise... >PASCAL: >type Complex = record RE, IM: real end; >PROLOG: >complex(RE, IM) :- real(RE), real(IM). The point of some of the previous postings is that the lookup for this kind of thing may be too expensive -- ie. O(n) where n is the size of the program, if we're implementing it naively, rather than a small constant in the case of pointers. Even if we had efficient lookup for special predicates used in this way, there would still be the problem of building such data structures at runtime (with assert and retract?). I'm afraid the ideal is still the use of looping data structures as actual data objects (that can be passed around as parameters). Some logical description of the types may still be possible, but that's different than using the existing predicate mechanisms to do looping data objects. >Also, if you consult the lambda calculus and functional programming literature, >you'll find out about results concerning the correspondence (isomorphism) >between types and propositions which underlies this observation >(records <-> AND, unions/variants <-> OR, functions <-> IMPLICATION, etc.) Hmm. This "Curry-Howard" isomorphism is really about treating formulae (A, B, C) as "types", the data objects of types A, B, C being formal descriptions of the proofs of A, B, C. The fact that these formal descriptions of proofs take the form of records, unions etc. is incidental -- no general data structures are necessarily being encoded. Curry-Howard does make proofs of type membership and proofs of formulae into the same thing. But in a logic programming setting this reduces to using a type-theoretic (say, ML-style) type discipline for data object types. This is the approach advocated by people like Frank Pfenning. From your remarks about flexibility, I think what you're talking about is more like Uday Reddy et al.'s approach of using predicate-definition-like constructs to describe types. --Jamie. jha@cs.ed.ac.uk "'He acts crazy, I guess. We all act crazy. I guess God acts crazy.' Etc."
lescanne@poincare.crin.fr (Pierre Lescanne) (03/07/91)
RTA-91: PRELIMINARY PROGRAM Fourth International Conference on Rewriting Techniques and Applications April 10-12, 1991 Como, Italy For information about registration, etc., see below or contact Professor G. Degli Antoni or Dr. Marelva Bianchi Dipartimento di Scienze dell'Informatione Universita degli Studi di Milano Via Moretto da Brescia, 9 I - 20133 Milano, Italy Telephone: +39.2.7575.201 / 209 +39.2.7575.257 FAX: +39.2.7611.0556 e-mail: gdantoni@imisiam.BITNET WEDNESDAY, 10 APRIL ___________________ ___________________ 8:30-8:45 Opening. SESSION 1 G. Smolka (U. Saarbrucken), Chair. 8:45-9:10 Transfinite reductions in orthogonal term rewriting systems. J. R. Kennaway (U. East Anglia), J. W. Klop (CWI, Amsterdam), M. R. Sleep (U. East Anglia), and F. J. de Vries (CWI, Amsterdam) 9:15-9:40 Redex captured in term graph rewriting. W. Farmer and R. Watro (MITRE Corp., Bedford) 9:45-10:10 Rewriting, narrowing, and equational unification: the higher-order cases. D. A. Wolfram (Oxford U.) 10:15-10:40 Adding algebraic rewriting to the untyped lambda calculus. D. Dougherty (Wesleyan U.) 10:40-11:10 BREAK SESSION 2 L. Bachmair (SUNY at Stony Brook), Chair. 11:10-11:35 Incremental termination proofs and the length of derivations. F. Drewes (U. Bremen) and C. Lautemann (U. Mainz) 11:40-12:05 Time bounded rewrite systers and termination proofs by generalized embedding. D. Hofbauer (TU Berlin) 12:10-12:35 Detecting redundant narrowing derivations by the LSE-SL test. A. Bockmayr and S. Krischer (U. Karlsruhe) 12:35-14:30 LUNCH SESSION 3 U. Martin (U. London and MIT), Chair. 14:30-14:55 Unification, weak unification, upper bound, lower bound, and generalization problems. F. Baader (U. Kaiserslautern) 15:00-15:25 AC unification through order-sorted AC1 unification. E. Domenjoud (CNRS and INRIA, Nancy) 15:30-15:55 Narrowing directed by a graph of terms. J. Chabin and P. Rety (U. Orlans) 16:00-16:25 How algebra can help in equational unification. F. Baader and W. Nutt (U. Kaiserslautern) 16:25-16:55 BREAK SESSION 4 C. Kirchner (INRIA, Nancy), Chair. 16:55-17:20 Undecidable properties of syntactic theories. F. Klay (INRIA, Nancy) 17:25-17:50 Goal directed strategies for paramodulation. W. Snyder and C. Lynch (Boston U.) 17:55-18:20 Minimal solutions of linear diophantine systems: bounds and algorithms. L. Pottier (INRIA, Sophia Antipolis) ________________________________________________________ THURSDAY, 11 APRIL SESSION 5 H. Ganzinger (U. Dortmund), Chair. 8:30-8:55 Proofs in parametrized specifications. H. Kirchner (CNRS and INRIA, Nancy) 9:00-9:25 Completeness of combinations of constructor systems. A. Middeldorp (CWI, Amsterdam) and Y. Toyama (CWI, Amsterdam and NTT Labs.) 9:30-9:55 Modular higher-order E-unification. T. Nipkow (U. Cambridge) and Z. Qian (U. Bremen) 10:00-10:25 On confluence for weakly normalizing systems. P-L Curien (CNRS, Paris) and G. Ghelli (U. Pisa) 10:25-10:55 BREAK SESSION 6 L. Bachmair (Stony Brook), Chair. 10:55-11:20 Program transformation and rewriting. F. Bellegarde (Oregon Grad. Inst.) 11:25-11:50 An efficient representation of arithmetic for term rewriting. D. Cohen (Royal Holloway and Bedford New College) and P. Watson (Glasgow U.) 11:55-12:20 Query optimization using conditional and unconditional rewrite rules. S. van Denneheuval, K. Kwast, E. Spaan (U. Amsterdam), and Renardel de Lavalette (U. Utrecht) 12:20-14:30 LUNCH SESSION 7: F. Otto (U. Kassel), Chair 14:30-14:55 Boolean algebra admits no canonical term rewriting system. R. Socher-Ambrosius (U. Kaiserslautern and SUNY, Stony Brook) 15:00-15:25 Decidability of confluence and termination of monadic term rewriting systems. K. Salomaa (U. Turku) 15:30-15:55 Bottom-up tree pushdown automata and rewrite systems. J-L Coquide, M. Dauchet, R. Gilleron ( U. Lille ), and S. Vagvolgyi (Hungerian Acad. Sci., Szeged) 16:00-16:25 On relationship between term rewriting systems and regular tree languages. G. Kucherov (USSR Acad. Sci., Novosibirsk) 16:25-16:55 BREAK SESSION 8 R. Book (UC Santa Barbara), Chair. 17:00-17:25 The equivalence of boundary and confluent graph grammars on graph languages with bounded degree. F. Brandenburg, U. Passau 17:30-17:55 Left-to-right tree pattern matching. A. Graef (U. Mainz) 18:00-18:25 Incremental techniques for efficient normalization of nonlinear rewrite systems. R. Ramesh (U. Texas - Dallas) and I.V. Ramakrishnan (SUNY at Stony Brook) _______________________________________________________ FRIDAY. 12 APRIL SESSION 9 F. Winkler (U. Linz), Chair. 8:45-9:10 On fairness of completion-based theorem proving strategies. M. P. Bonacina (U. Milano and SUNY at Stony Brook) and J. Hsiang (SUNY at Stony Brook) 9:15-9:40 Proving inductive theorems by completion and embedding techniques. J. Avenhaus (U. Kaiserslautern) 9:45-10:10 Divergence phenomena during completion. A. Sattler-Klein (U. Kaiserslautern) 10:15-10:40 Simulating Buchberger's algorithm by Knuth-Bendix completion. R. Buendgen (U. Tuebingen) 10:40-11:10 BREAK SESSION 10 C. Kirchner (INRIA, Nancy), Chair. 11:10-11:35 On proving properties of completion strategies. M. Hermann (CNRS and INRIA, Nancy) 11:40-12:05 On AC-termination and ground AC-completion. C. Marche (U. Paris-Sud) 12:10-12:35 Any ground associative-commutative theory has a finite canonical system. P. Narendran (SUNY at Albany) and M. Rusinowitch (CNRS and INRIA, Nancy) FINI ________________________________________________________ SYSTEMS DEMONSTRATIONS A narrowing-based theorem prover. U. Fraus (U. Passau) and H. Hussmann (TU Muenchen) ANIGRAF: An interactive systerm for the animation of graph rewriting systems with priorities. M. Billaud (U. Bordeaux) EMMY: A refutational theorem prover for first-order logic with equations. A. Deruyer (U. Lille and SUNY at Stony Brook) The Tecton Proof System. R. Agarwal (Rensselaer Poly. Inst.), D. Kapur (SUNY at Albany), D. Musser (Rensselaer Poly. Inst.), X. Nie (SUNY at Albany) ============================================================================== RTA '91 - Conference registration form Please send this registration form with payment to: Centro di Cultura Scientifica "A. Volta" - Villa Olmo, Via Cantoni 1 - 22100 Como (Italy). Advanced registration discount are available to all registration forms received, with full payment, post-marked on or before 28/02/1991. Please bring your registration acknowledgment with you. Notices on cancellation must be received in writing at Centro "A. Volta" before 15/03/1991. Registration fees will include proceedings, lunches, dinners, additional informative material, on site reception hostesses. First name _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Surname _ _ _ _ _ _ _ _ _ _ _ Position _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Institution _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Address _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ City _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ State _ _ _ _ _ _ _ _ _ _ _ Zip _ _ _ _ _ Phone _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Telex _ _ _ _ _ _ _ _ Fax _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ E-mail _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Please specify society name and name of Association (EATCS, IEEE, ACM, SIGART, ...) : Society name _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Association _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Proceedings A preprint copy of the Conference proceedings - edited by Springer Verlag - will be distributed to the attendees. Supplementary copies can be bought on site. Payment Please send the amount corresponding to the full amount of the registration by: International Postal Money Order or Eurocheque. Payment should be addressed to Centro di Cultura Scientifica "A. Volta" - Villa Olmo, Via Cantoni 1 - 22100 Como (Italy) and be effected in italian liras net of all bank charges (if not possible, U.S. dollars will be accepted). Further possibility is payment by Banker's draft drawn on Banco Lariano - P.zza Cavour 15 - 22100 Como (Italy) - c/c 479619/3 headed to "Centro di Cultura Scientifica Alessandro Volta"; in this case, please consider high bank charges. A check or money order must accompany your registration form. REGISTRATION FEES RTA '91 Advanced registration On site registration Attendees Lit. 300.000 Lit. 350.000 Lecturers Lit. 230.000 Lit. 280.000 Commitee members Lit. 200.000 Lit. 230.000 -- Pierre LESCANNE | Tel: (work) (33) 83 59 30 07 CRIN (CNRS) & INRIA-Lorraine | (home) (33) 83 22 76 92 BP 239 | Fax: (33) 83 27 83 19 F54506 VANDOEUVRE-les-NANCY Cedex FRANCE | E-mail: lescanne@loria.crin.fr