Related papers: Higher-Order Pattern Complement and the Strict Lam…
Many theories of semantic interpretation use lambda-term manipulation to compositionally compute the meaning of a sentence. These theories are usually implemented in a language such as Prolog that can simulate lambda-term operations with…
We propose a purely extensional semantics for higher-order logic programming. In this semantics program predicates denote sets of ordered tuples, and two predicates are equal iff they are equal as sets. Moreover, every program has a unique…
This paper obtains a completeness result for inequational reasoning with applicative terms without variables in a setting where the intended semantic models are the full structures, the full type hierarchies over preorders for the base…
We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. The…
We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of…
The Functional Machine Calculus (Heijltjes 2022) is a new approach to unifying the imperative and functional programming paradigms. It extends the lambda-calculus, preserving the key features of confluent reduction and typed termination, to…
We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming…
We know extensions of first order logic by quantifiers of the kind "there are uncountable many ...", "most ..." with new axioms and appropriate semantics. Related are operations such as "set of x, such that ...", Hilbert's…
The lambda calculus is a widely accepted computational model of higher-order functional pro- grams, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda…
Identifying structural parameters in linear simultaneous-equation models is a longstanding challenge. Recent work exploits information in higher-order moments of non-Gaussian data. In this literature, the structural errors are typically…
Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the…
We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of…
We give a simple order-theoretic construction of a Cartesian closed category of sequential functions. It is based on bistable biorders, which are sets with a partial order -- the extensional order -- and a bistable coherence, which captures…
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative…
A non-deterministic call-by-need lambda-calculus \calc with case, constructors, letrec and a (non-deterministic) erratic choice, based on rewriting rules is investigated. A standard reduction is defined as a variant of left-most outermost…
To answer database queries over incomplete data the gold standard is finding certain answers: those that are true regardless of how incomplete data is interpreted. Such answers can be found efficiently for conjunctive queries and their…
A number of first-order calculi employ an explicit model representation formalism for automated reasoning and for detecting satisfiability. Many of these formalisms can represent infinite Herbrand models. The first-order fragment of…
Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactically and semantically. At the same time assertions have been in use for some time in (C)LP systems helping programmers…
A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely…
We prove the undecidability of the third order pattern matching problem in typed lambda-calculi with dependent types and in those with type constructors by reducing the second order unification problem to them.