Lecture

Termination Analysis using Dependency Pairs

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Description

This lecture covers automated termination analysis of programs using dependency pairs, starting with classical and modern techniques for term rewriting. It explores the concept of dependency pairs, the annual termination competition, and automated tools like AProVE. The lecture delves into termination analysis for imperative and functional programming languages, discussing direct and transformational approaches. It also explains techniques for transforming logic programs to term rewriting systems and termination graphs, emphasizing the importance of dependency pairs in logic programming. The lecture concludes with insights on transforming Haskell programs to term rewriting systems and termination graphs, showcasing the advancements in automated termination analysis.

Official source

Ontological neighbourhood

Theoretical computer science

Programming language theory: High-level programming languages

Related concepts (32)

Rewriting

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or reduction systems). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects. Rewriting can be non-deterministic. One rule to rewrite a term could be applied in many different ways to that term, or more than one rule could be applicable.

Programming language

A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming language is usually split into the two components of syntax (form) and semantics (meaning), which are usually defined by a formal language. Some languages are defined by a specification document (for example, the C programming language is specified by an ISO Standard) while other languages (such as Perl) have a dominant implementation that is treated as a reference.

Abstract rewriting system

In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting systems. In its simplest form, an ARS is simply a set (of "objects") together with a binary relation, traditionally denoted with ; this definition can be further refined if we index (label) subsets of the binary relation.

Functional programming

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program. In functional programming, functions are treated as first-class citizens, meaning that they can be bound to names (including local identifiers), passed as arguments, and returned from other functions, just as any other data type can.

Confluence (abstract rewriting)

In computer science, confluence is a property of rewriting systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system. The usual rules of elementary arithmetic form an abstract rewriting system. For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses; however, in both cases the same result is eventually obtained.

Related lectures (64)

Functional Programming: Concepts and Implementation

Covers the concepts and implementation of functional programming in Scala, emphasizing functions, immutable data, and data abstraction.

Stainless Verification System Tutorial

Introduces Stainless, an open-source tool for verifying Scala programs, covering language, modeling, verification tips, and inner workings.

Introduction to Coq: Arithmetic Expressions and Evaluators

Covers the basics of Coq, focusing on arithmetic expressions, evaluation, and proof techniques.

Semantics in Computer Language Processing: Understanding Meaning

Covers the semantics of programming languages, focusing on the Add language and the role of rewriting rules and CK machines in understanding meaning.

Introduction to Types and Inductive Relations