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 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 Experiments with ZF Set Theory in HOL and Isabelle

1995 ◽  
Vol 2 (37) ◽  
Author(s):  
Sten Agerholm ◽  
Mike Gordon
Keyword(s):  
Set Theory ◽  
Lambda Calculus ◽  
General Purpose ◽  
Higher Order ◽  
Proof Assistants ◽  
Higher Order Logic ◽  
First Order ◽  
Advantages And Disadvantages ◽  
Theory Versus

Most general purpose proof assistants support versions of<br />typed higher order logic. Experience has shown that these logics are capable<br />of representing most of the mathematical models needed in Computer<br />Science. However, perhaps there exist applications where ZF-style<br />set theory is more natural, or even necessary. Examples may include<br />Scott's classical inverse-limit construction of a model of the untyped lambda-calculus<br /> (D_inf) and the semantics of parts of the Z specification notation.<br /><br />This paper compares the representation and use of ZF set theory within<br />both HOL and Isabelle. The main case study is the construction of D_inf.<br />The advantages and disadvantages of higher-order set theory versus first-order<br />set theory are explored experimentally. This study also provides a<br />comparison of the proof infrastructure of HOL and Isabelle.

Fractional fractals

2020 ◽  
Vol 23 (5) ◽  
pp. 1329-1348
Author(s):  
J.A. Tenreiro Machado ◽  
Daniel Cao Labora
Keyword(s):  
Fractional Derivative ◽  
Iterated Function System ◽  
Main Idea ◽  
Higher Order ◽  
Numerical Calculations ◽  
Function System ◽  
Limit Sets ◽  
First Order ◽  
Iterated Function

Abstract This paper introduces the notion of “fractional fractals”. The main idea is to establish a connection between the classical iterated function system and the first order truncation of the Gründwald-Letnikov fractional derivative. This allows us to consider higher order truncations, and also to study the limit sets for these higher order systems. We prove several results involving the existence and dimension of such limit sets, that will be called “fractional fractals”. Some numerical calculations and representations illustrate relevant examples.

scholarly journals Towards Strong Higher-Order Automation for Fast Interactive Verification

10.29007/3ngx ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette ◽  
Pascal Fontaine ◽  
Stephan Schulz ◽  
Uwe Waldmann
Keyword(s):  
Research Council ◽  
Higher Order ◽  
Point Of View ◽  
Satisfiability Modulo Theories ◽  
Proof Assistants ◽  
First Order ◽  
The Core ◽  
Proof Rules ◽  
Level Of Automation ◽  
Smt Solvers

We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. From this point of view, it seems desirable to enrich superposition and SMT (satisfiability modulo theories) with higher-order reasoning in a careful manner, to preserve their good properties. Representative benchmarks from the interactive community can guide the design of proof rules and strategies. With higher-order superposition and higher-order SMT in place, highly automatic provers could be built on modern superposition provers and SMT solvers, following a stratified architecture reminiscent of that of modern SMT solvers. We hope that these provers will bring a new level of automation to the users of proof assistants. These challenges and work plan are at the core of the Matryoshka project, funded for five years by the European Research Council. We encourage researchers motivated by the same goals to get in touch with us, subscribe to our mailing list, and join forces.

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