On two forms of structural recursion

1995 ◽  
pp. 111-124 ◽  
Author(s):  
Dan Suciu ◽  
Limsoon Wong
Keyword(s):  
Structural Recursion

Structures for structural recursion

2015 ◽  
Vol 50 (9) ◽  
pp. 127-139
Author(s):  
Paul Downen ◽  
Philip Johnson-Freyd ◽  
Zena M. Ariola
Keyword(s):  
Structural Recursion

First-order unification by structural recursion

2003 ◽  
Vol 13 (6) ◽  
pp. 1061-1075 ◽  
Author(s):  
CONOR MCBRIDE
Keyword(s):  
First Order ◽  
Structural Recursion

Efficient implementation of structural recursion

1987 ◽  
pp. 204-213
Author(s):  
K. Indermark ◽  
H. Klaeren
Keyword(s):  
Efficient Implementation ◽  
Structural Recursion

Generic top-down discrimination for sorting and partitioning in linear time

2012 ◽  
Vol 22 (3) ◽  
pp. 300-374 ◽  
Author(s):  
FRITZ HENGLEIN
Keyword(s):  
Linear Time ◽  
Source Code ◽  
Equivalence Relations ◽  
Asymptotic Performance ◽  
Data Types ◽  
Worst Case ◽  
First Order ◽  
Structural Recursion ◽  
Algebraic Data Types ◽  
Abstract Types

AbstractWe introduce the notion ofdiscriminationas a generalization of both sorting and partitioning, and show thatdiscriminators(discrimination functions) can be definedgenerically, by structural recursion on representations oforderingandequivalence relations. Discriminators improve the asymptotic performance of generic comparison-based sorting and partitioning, and can be implemented not to expose more information than the underlying ordering, respectively equivalence relation. For a large class of order and equivalence representations, including all standard orders for regular recursive first-order types, the discriminators execute in the worst-case linear time. The generic discriminators can be coded compactly using list comprehensions, with order and equivalence representations specified using Generalized Algebraic Data Types. We give some examples of the uses of discriminators, including the most-significant digit lexicographic sorting, type isomorphism with an associative-commutative operator, and database joins. Source code of discriminators and their applications in Haskell is included. We argue that built-in primitive types, notably pointers (references), should come with efficient discriminators, not just equality tests, since they facilitate the construction of discriminators for abstract types that are both highly efficient and representation-independent.

scholarly journals Vector Programming Using Structural Recursion

2018 ◽  
Vol 270 ◽  
pp. 1-17 ◽  
Author(s):  
Marco T. Morazán
Keyword(s):  
Structural Recursion

NOMINAL STRUCTURES AND STRUCTURAL RECURSION

1994 ◽  
Vol 10 (4) ◽  
pp. 453-470 ◽  
Author(s):  
Robert Frank ◽  
Anthony Kroch
Keyword(s):  
Structural Recursion

scholarly journals Structural recursion with locally scoped names

2011 ◽  
Vol 21 (3) ◽  
pp. 235-286 ◽  
Author(s):  
ANDREW M. PITTS
Keyword(s):  
Programming Languages ◽  
Simple Interpretation ◽  
Nominal System ◽  
Structural Recursion ◽  
Recursive Definitions ◽  
Nominal Sets

AbstractThis paper introduces a new recursion principle for inductively defined data modulo α-equivalence of bound names that makes use of Odersky-style local names when recursing over bound names. It is formulated in simply typed λ-calculus extended with names that can be restricted to a lexical scope, tested for equality, explicitly swapped and abstracted. The new recursion principle is motivated by the nominal sets notion of ‘α-structural recursion’, whose use of names and associated freshness side-conditions in recursive definitions formalizes common practice with binders. The new calculus has a simple interpretation in nominal sets equipped with name-restriction operations. It is shown to adequately represent α-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. The paper is a revised and expanded version of Pitts (Nominal System T. In Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 2010 (Madrid, Spain). ACM Press, pp. 159–170, 2010).

scholarly journals Structural Recursion on Ordered Trees and List-Based Complex Objects

2006 ◽  
pp. 344-358
Author(s):  
Edward L. Robertson ◽  
Lawrence V. Saxton ◽  
Dirk Van Gucht ◽  
Stijn Vansummeren
Keyword(s):  
Complex Objects ◽  
Ordered Trees ◽  
Structural Recursion

Modelling general recursion in type theory

2005 ◽  
Vol 15 (4) ◽  
pp. 671-708 ◽  
Author(s):  
ANA BOVE ◽  
VENANZIO CAPRETTA
Keyword(s):  
Programming Language ◽  
Type Theory ◽  
Functional Programming ◽  
Recursive Algorithm ◽  
Recursive Algorithms ◽  
Constructive Type Theory ◽  
Structural Recursion ◽  
Constructive Type ◽  
Definition Of ◽  
Theoretic Version

Constructive type theory is an expressive programming language in which both algorithms and proofs can be represented. A limitation of constructive type theory as a programming language is that only terminating programs can be defined in it. Hence, general recursive algorithms have no direct formalisation in type theory since they contain recursive calls that satisfy no syntactic condition guaranteeing termination. In this work, we present a method to formalise general recursive algorithms in type theory. Given a general recursive algorithm, our method is to define an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm is then defined by structural recursion on the proof that the input values satisfy this predicate. The method separates the computational and logical parts of the definitions and thus the resulting type-theoretic algorithms are clear, compact and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Here, we give a formal definition of the method and discuss its power and its limitations.

Sign in / Sign up

Export Citation Format

Share Document