Functional and Logic Programming: 6th International Symposium, FLOPS 2002, Aizu, Japan, September 15-17, 2002. Proceedings (Lecture Notes in Computer Science, 2441)

This Volume Contains The Proceedings Of The Sixth Fuji International Sym- Sium On Functional And Logic Programming (flops 2002), Held In Aizu, Japan, September 15–17, 2002, Hosted By The University Of Aizu, And Colocated With The First Asian Symposium On Partial Evaluation Semantics-based Program Manipulation (asia-pepm 2002), Which Was Held On September 12–14. Flops Is A Forum For Research On All Issues Concerning Functional Progr- Ming And Logic Programming. In Particular, It Aims To Stimulate The Cro- Fertilization As Well As The Integration Of The Two Paradigms. The Previous Flops Meetings Took Place In Fuji-susono (1995), Shonan (1996), Kyoto (1998), Tsukuba (1999), And Tokyo (2001). The Proceedings Of Flops ’99 And Flops 2001 Were Published By Springer-verlag As Lecture Notes In Computer Science, Vols. 1722 And 2024, Respectively. There Were 27 Submissions, And These Came From Australia (1), Brazil (1), 1 China (1), Denmark (2), Germany (1 ), Italy (1), Japan (6), Korea (1), Por- 2 2 1 1 Tugal (2), Russia ( ), Spain (6), Sweden (1), The Uk (2 ), And The Usa ( ). Invited Papers -- Formal Methods In Cafeobj -- The Essence Of Xml (preliminary Version) -- To The Gates Of Hal: A Hal Tutorial -- Tutorial Paper -- Functional Logic Design Patterns -- Constraints -- On Consistency And Width Notions For Constraint Programs With Algebraic Constraints -- Solving Mixed Quantified Constraints Over A Domain Based On Eal Numbers And Erbrand Terms -- Program Transformation And Analysis -- On The Correctness Of The Factoring Transformation -- Lambda-lifting In Quadratic Time -- Semantics -- The Well-founded Semantics In Normal Logic Programs With Uncertainty -- Linearly Used Effects: Monadic And Cps Transformations Into The Linear Lambda Calculus -- Coinductive Interpreters For Process Calculi -- Rewriting -- Descendants And Head Normalization Of Higher-order Rewrite Systems -- Narrowing Failure In Functional Logic Programming -- Compilation Techniques -- The Hipe/x86 Erlang Compiler: System Description And Performance Evaluation -- Dynamic-cut With Definitional Trees -- Programming Methodology -- The Head Condition And Polymorphic Recursion -- Structural Abstraction And Application In Logic Programming -- Vm?: A Functional Calculus For Scientific Discovery. Zhenjiang Hu, Mario Rodr Iguez-artalejo (eds.) Lecture Notes in Computer Science Preface Organization Table of Contents Formal Methods in CafeOBJ Formal Methods in CafeOBJ Introduction Design Considerations for Formal Specification Language Systems A Brief History of CafeOBJ Language Important Features of CafeOBJ Language Basic Constructs of CafeOBJ Language An Example of Verification in Initial Models: Equivalence of Two Definitions of Factorial An Example of Verification in Behavioral Specification: Simple Bank Account An Example of Verification in Behavioral Concurrent Object Composition: Compositional Bank Account Proving Behavioral Properties for the Composed Object Conclusion The Essence of XML (Preliminary Version) The Essence of XML (Preliminary Version) Introduction XML Schema by Example Values and Types Values Types Top Level Definitions Built-In Type Declarations Relationships between Names Element Name Sets Derives Auxiliary Judgments Yields Resolution Matches Erasure Simply Erases Erases Validation Simply Validate Validate Ambiguity and the Validation Theorem To the Gates of HAL: A HAL Tutorial To the Gates of HAL: A HAL Tutorial Introduction A First Example Declarations Constraint Solvers and Type Classes Dynamic Scheduling Herbrand Constraint Solving The Solver Hierarchy Writing Constraint Solvers in HAL Current System Conclusion Functional Logic Design Patterns Functional Logic Design Patterns Introduction Functional Logic Programming and Curry Patterns Constrained Constructor Concurrent Distinct Choices Incremental Solution Locally Defined Global Identifier Opaque Type Exemplary Programs Conclusion Further Search Strategies for the Incremental Solution Pattern On Consistency and Width Notions for Constraint Programs with Algebraic Constraints On Consistency and Width Notions for Constraint Programs with Algebraic Constraints Introduction Algebraic Constraint Satisfaction Problems; Width-Notion and Consistency Freuder's and Faltings' Settings Extension to Algebraic CSPs; Consistency and Complexity A New Width Notion for Algebraic CSPs Solving Mixed Quantified Constraints over a Domain Based on Real Numbers and Herbrand Terms Solving Mixed Quantified Constraints over a Domain Based on Real Numbers and Herbrand Terms Introduction The Constraint System RH A Solving Procedure for RH-Constraints Solved Forms, Basic Formulas and Elemental Constraints Eliminating Quantifiers The Transformation Algorithm Examples Conclusion On the Correctness of the Factoring Transformation On the Correctness of the Factoring Transformation Introduction Preliminaries Terms, Substitutions and Positions Term Rewriting, Classes of Term Rewrite Systems and Programs Functional Logic Programming The Factoring Transformation Correctness of the Factoring Transformation Embedding Relation Completeness Soundness Discussion Conclusions Lambda-Lifting in Quadratic Time Lambda-Lifting in Quadratic Time Lambda-Lifting Setting and Background Three Examples Overview Lambda-Lifting in Cubic Time Johnsson's Parameter-Lifting Algorithm An Alternative Specification Based on Graphs Example Lambda-Lifting in Quadratic Time Complexity Analysis Lower Bound Contribution The New Algorithm Revisiting the Example of Section 2.3 Related Work Supercombinator Conversion Closure Conversion Lambda-Dropping Mixed Style Correctness Issues Conclusion and Future Work Graph Algorithms The Well-Founded Semantics in Normal Logic Programs with Uncertainty The Well-Founded Semantics in Normal Logic Programs with Uncertainty Introduction Preliminaries Interpretations of Programs Alternating Fixpoint and Compromise Semantics Immediate Consequence Operators Compromise Semantics of an np-Program Comparison with Existing Semantics Conclusions Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus Introduction Background: Linearly Used Effects A Framework for Linearly Used Effects Fully Complete CPS Transformation Semantics of Linearly Used Effects Models of Linear Type Theory, and Monads A Monad for Linearly Used Continuations The Calculi The Computational Lambda Calculus The Linear Lambda Calculus Monadic and CPS Transformations Monadic Transformations The CPS Transformation Full Completeness Adding Recursion Classifying Effects via Linearity Concluding Remarks The Inversion Function Coinductive Interpreters for Process Calculi Coinductive Interpreters for Process Calculi Introduction Preliminaries Processes and Combinators Processes Interaction Dynamic Combinators Static Combinators A Process Language Conclusions The Interpreter Descendants and Head Normalization of Higher-Order Rewrite Systems Descendants and Head Normalization of Higher-Order Rewrite Systems Introduction Preliminaries Descendant Head Normalization Head-Needed Redex Head Normalizing Strategy Proof of Lemma 2 Proof of Lemma 7 Narrowing Failure in Functional Logic Programming Narrowing Failure in Functional Logic Programming Introduction Technical Preliminaries A Semantic Framework for FLP with Failure Set Expressions Programs Proof Calculus for Programs and Set-Expressions Operational Semantics Contexts A Narrowing Relation for Set-Expressions Correctness and Completeness of Snarr Conclusions and Future Work The HiPE/x86 Erlang Compiler: System Description and Performance Evaluation The HiPE/x86 Erlang Compiler: System Description and Performance Evaluation Introduction The Erlang Language and Erlang/OTP HiPE: Brief System Overview HiPE/x86 Runtime Architecture Register Usage Calling Convention Stack Frames and Stack Descriptors Garbage Collection and Generational Stack Scanning Exception Handling C and Unix Interface Issues The HiPE/x86 Code Generator Backend Intermediate Representation Register Allocation Frame Management Linearising the Code Assembling the Code Planned Future Improvements Performance Evaluation Related Systems Concluding Remarks Dynamic-Cut with Definitional Trees Dynamic-Cut with Definitional Trees Introduction Preliminaries Motivating Examples Detecting Deterministic Functions A Prolog Implementation of Dynamic Cut The Translation Scheme Generating Prolog Code Examples Experimental Results Conclusions The Head Condition and Polymorphic Recursion The Head Condition and Polymorphic Recursion Introduction Typed Logic and Functional Programming The Head Condition Polymorphic Recursion Digression: Polymorphic Recursion in the Usual FP Formalism Polymorphic Recursion in Our Formalism Relating the Two Conditions A Special Kind of Term Language Calls and Answers The Magic Transformation Conclusion Structural Abstraction and Application in Logic Programming Structural Abstraction and Application in Logic Programming Introduction Syntax and Semantics Structural Abstraction Structural Rewrite Semantics Structural Operators Explicit Application Implicit Application --- Pipes Mode Switch Meta Structures Escape from Application Exploring the Framework with New Operators Implementation Applicability --- Final Remarks Generators Programmable Rewrite --- Equating Abstractions VMλ: A Functional Calculus for Scientific Discovery VM: A Functional Calculusfor Scientific Discovery Introduction Simple VMLambda Syntax and Informal Semantics Operational Semantics Type System VMLambdaabl: An Extension of Simple VMLambda with Labeled Arguments Syntax Semantics Type System Translation of VMLambdaabl into OCaml Related Work and Future Work Author Index Constituting the proceedings of the 6th International Symposium on Functional and Logic Programming, held in Aizu, Japan, this volume contains 15 revised full papers and three full invited papers, covering program transformation and analysis, semantics, rewriting and compilation techniques.