scholarly journals A Simple Correctness Proof of the Direct-Style Transformation

2002 ◽  
Vol 9 (2) ◽  
Author(s):  
Lasse R. Nielsen
Keyword(s):  
Program Transformation ◽  
Higher Order ◽  
Correctness Proof ◽  
First Order ◽  
Structural Induction ◽  
Higher Order Functions

We build on Danvy and Nielsen's first-order program transformation into continuation-passing style (CPS) to present a new correctness proof of the converse transformation, i.e., a one-pass transformation from CPS back to direct style. Previously published proofs were based on, e.g., a one-pass higher-order CPS transformation, and were complicated by having to reason about higher-order functions. In contrast, this work is based on a one-pass CPS transformation that is both compositional and first-order, and therefore the proof simply proceeds by structural induction on syntax.

scholarly journals A First-Order One-Pass CPS Transformation

2001 ◽  
Vol 8 (49) ◽  
Author(s):  
Olivier Danvy ◽  
Lasse R. Nielsen
Keyword(s):  
Control Flow ◽  
Logical Relation ◽  
Correctness Proof ◽  
First Order ◽  
Structural Induction ◽  
Flow Information

We present a new transformation of call-by-value lambda-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation.<br /> <br />This new CPS transformation connects two separate lines of research. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.

scholarly journals Defunctionalization at Work

2001 ◽  
Vol 8 (23) ◽  
Author(s):  
Olivier Danvy ◽  
Lasse R. Nielsen
Keyword(s):  
Program Transformation ◽  
Higher Order ◽  
Practical Applications ◽  
First Order ◽  
Correctness Proofs

We study practical applications of Reynolds's defunctionalization technique, which is a whole-program transformation from higher-order to first-order functional programs. This study leads us to discover new connections between seemingly unrelated higher-order and first-order specifications and their correctness proofs. We thus perceive defunctionalization both as a springboard and as a bridge: as a springboard for discovering new connections between the first-order world and the higher-order world; and as a bridge for transferring existing results between first-order and higher-order settings.

scholarly journals A Denotational Investigation of Defunctionalization

2000 ◽  
Vol 7 (47) ◽  
Author(s):  
Lasse R. Nielsen
Keyword(s):  
Data Structures ◽  
Program Transformation ◽  
Denotational Semantics ◽  
Higher Order ◽  
Functional Language ◽  
First Order

<p>Defunctionalization was introduced by John Reynolds in his 1972<br />article Definitional Interpreters for Higher-Order Programming <br />Languages. Defunctionalization transforms a higher-order program into a first-order one, representing functional values as data structures. Since then it has been used quite widely, but we observe that it has never been proven correct. We formalize defunctionalization denotationally for a typed functional language, and we prove that it preserves the meaning of any terminating program. Our proof uses logical relations.</p><p>Keywords: defunctionalization, program transformation, denotational semantics, logical relations.</p>

scholarly journals Functions-as-constructors higher-order unification: extended pattern unification

2021 ◽  
Author(s):  
Tomer Libal ◽  
Dale Miller
Keyword(s):  
Main Idea ◽  
Free Variable ◽  
Higher Order ◽  
Proof Assistants ◽  
Computational Logic ◽  
First Order ◽  
Term Structures ◽  
Logic Systems ◽  
Higher Order Functions

AbstractUnification is a central operation in constructing a range of computational logic systems based on first-order and higher-order logics. First-order unification has several properties that guide its incorporation in such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respects the laws governing λ-binding (i.e., the equalities for α, β, and η-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been used in numerous implemented systems and in various theoretical settings, it is too weak for many applications. This paper defines an extension of pattern unification that should make it more generally applicable, especially in proof assistants that allow for higher-order functions. This extension’s main idea is that the arguments to a higher-order, free variable can be more than just distinct bound variables. In particular, such arguments can be terms constructed from (sufficient numbers of) such bound variables using term constructors and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.

scholarly journals Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem

10.29007/t4gz ◽  
2018 ◽  
Author(s):  
Geoff Hamilton ◽  
Morten Heine Sørensen
Keyword(s):  
Program Transformation ◽  
Infinite Sequence ◽  
Lambda Calculus ◽  
Higher Order ◽  
New Technique ◽  
Transformation Technique ◽  
First Order ◽  
Auxiliary Functions ◽  
Order Language ◽  
A New Technique

A program transformation technique should terminate, return efficient output programs and be efficient itself.For positive supercompilation ensuring termination requires memoisation of expressions, and these are subsequently used to determine when to perform generalization and folding. For a first-order language, every infinitesequence of transformation steps must include function unfolding, so it is sufficient to memoise only those expressions immediately prior to a function unfolding step.However, for a higher-order language, it is possible for an expression to have an infinite sequence of transformation steps which do not include function unfolding, so memoisation prior to a function unfolding step is not sufficient by itselfto ensure termination. But memoising additional expressions is expensive during transformation and may lead to less efficient output programs due to auxiliary functions. This additional memoisation may happen explicitly during transformationor implicitly via a pre-processing transformation as outlined in previous work by the first author.We introduce a new technique for local driving in higher-order positive supercompilation which obliviates the need for memoising other expressions than function unfolding steps, thereby improving efficiency of both the transformation and the generated programs. We exploit the fact, due to the second author in the setting of type-free lambda-calculus that every expression with an infinite sequence of transformation steps not involving function unfolding must have somthing like the term Omega = (lambda x. x x) (lambda x . x x) embedded within it in a certain sense. The technique has proven useful on a host of examples.

EDUCATIONAL PEARL: ‘Proof-directed debugging’ revisited for a first-order version

2006 ◽  
Vol 16 (6) ◽  
pp. 663-670 ◽  
Author(s):  
KWANGKEUN YI
Keyword(s):  
State Machine ◽  
Higher Order ◽  
Powerful Method ◽  
Introductory Programming ◽  
Final Version ◽  
First Order ◽  
Higher Order Functions

Some 10 years ago, Harper illustrated the powerful method of proof-directed debugging for developing programs with an article in this journal. Unfortunately, his example uses both higher-order functions and continuation-passing style, which is too difficult for students in an introductory programming course. In this pearl, we present a first-order version of Harper's example and demonstrate that it is easy to transform the final version into an efficient state machine. Our new version convinces students that the approach is useful, even essential, in developing both correct and efficient programs.

Even higher-order functions for parsing or Why would anyone ever want to use a sixth-order function?

1998 ◽  
Vol 8 (2) ◽  
pp. 195-199 ◽  
Author(s):  
CHRIS OKASAKI
Keyword(s):  
Functional Programming ◽  
Higher Order ◽  
Second Order ◽  
Sixth Order ◽  
Order Function ◽  
First Order ◽  
Higher Order Functions

A higher-order function is a function that takes another function as an argument or returns another function as a result. More specifically, a first-order function takes and returns base types, such as integers or lists. A kth-order function takes or returns a function of order k−1. Currying often artificially inflates the order of a function, so we will ignore all inessential currying. (Whether a particular instance of currying is essential or inessential is open to debate, but we expect that our choices will be uncontroversial.) In addition, when calculating the order of a polymorphic function, we instantiate all type variables with base types. Under these assumptions, most common higher-order functions, such as map and foldr, are second-order, so beginning functional programmers often wonder: What good are functions of order three or above? We illustrate functions of up to sixth-order with examples taken from a combinator parsing library.Combinator parsing is a classic application of functional programming, dating back to at least Burge (1975). Most combinator parsers are based on Wadler's list-of-successes technique (Wadler, 1985). Hutton (1992) popularized the idea in his excellent tutorial Higher-Order Functions for Parsing. In spite of the title, however, he considered only functions of up to order three.

Dual systems for all: Higher-order, role-based relational reasoning as a uniquely derived feature of human cognition

2019 ◽  
Vol 42 ◽  
Author(s):  
Daniel J. Povinelli ◽  
Gabrielle C. Glorioso ◽  
Shannon L. Kuznar ◽  
Mateja Pavlic
Keyword(s):  
Temporal Reasoning ◽  
Higher Order ◽  
Important Case ◽  
Human Cognition ◽  
Relational Reasoning ◽  
Dual Systems ◽  
First Order ◽  
Reasoning System ◽  
Role Based

Abstract Hoerl and McCormack demonstrate that although animals possess a sophisticated temporal updating system, there is no evidence that they also possess a temporal reasoning system. This important case study is directly related to the broader claim that although animals are manifestly capable of first-order (perceptually-based) relational reasoning, they lack the capacity for higher-order, role-based relational reasoning. We argue this distinction applies to all domains of cognition.

Challenging the Multidimensional Conception of Perceived Person-Environment Fit

2020 ◽  
pp. 1-9
Author(s):  
Julian M. Etzel ◽  
Gabriel Nagy
Keyword(s):  
Higher Education ◽  
University Students ◽  
Educational Outcomes ◽  
Factor Model ◽  
Higher Order ◽  
Substantial Proportion ◽  
Unique Variance ◽  
First Order ◽  
Person Environment Fit ◽  
Order Factor

Abstract. In the current study, we examined the viability of a multidimensional conception of perceived person-environment (P-E) fit in higher education. We introduce an optimized 12-item measure that distinguishes between four content dimensions of perceived P-E fit: interest-contents (I-C) fit, needs-supplies (N-S) fit, demands-abilities (D-A) fit, and values-culture (V-C) fit. The central aim of our study was to examine whether the relationships between different P-E fit dimensions and educational outcomes can be accounted for by a higher-order factor that captures the shared features of the four fit dimensions. Relying on a large sample of university students in Germany, we found that students distinguish between the proposed fit dimensions. The respective first-order factors shared a substantial proportion of variance and conformed to a higher-order factor model. Using a newly developed factor extension procedure, we found that the relationships between the first-order factors and most outcomes were not fully accounted for by the higher-order factor. Rather, with the exception of V-C fit, all specific P-E fit factors that represent the first-order factors’ unique variance showed reliable and theoretically plausible relationships with different outcomes. These findings support the viability of a multidimensional conceptualization of P-E fit and the validity of our adapted instrument.

Sign in / Sign up

Export Citation Format

Share Document