Applicative computing systems and technologies have taken a strong position in modern computing. In this paper, the basic applicative system, whether it is a lambdacalculus or a system of combinators, is considered a...
详细信息
Applicative computing systems and technologies have taken a strong position in modern computing. In this paper, the basic applicative system, whether it is a lambdacalculus or a system of combinators, is considered as a prototype concept system, using which it is possible to build individual systems that are practically significant for mathematics, computing, or programming. They are families of computational models that have both their own semantics and applied areas. This conceptualization/individualization technique is characteristic of the field of semantic studies. As it turns out, the applicative approach forms a metatheoretical framework that provides the basis for cognitive systems that consider abstract objects and interpret their properties and behavior in the environment of modern computing.
We present a name free lambda-calculus with explicit substitutions, based on a generalised notion of director strings. Terms are annotated with information - directors - that indicate how substitutions should be propa...
详细信息
We present a name free lambda-calculus with explicit substitutions, based on a generalised notion of director strings. Terms are annotated with information - directors - that indicate how substitutions should be propagated. We first present a calculus where we can simulate arbitrary beta-reduction steps, and then simplify the rules to model the evaluation of functional programs (reduction to weak head normal form). We also show that we can define the closed reduction strategy. This is a weak strategy which, in contrast with standard weak strategies, allows certain reductions to take place inside lambda-abstractions thus offering more sharing. Our experimental results confirm that, for large combinator-based terms, our weak evaluation strategies out-perform standard evaluators. Moreover, we derive two abstract machines for strong reduction which inherit the efficiency of the weak evaluators.
A system of equations in the lambda-calculus is a set of formulas of lambda (the equations) together with a finite set of variables of lambda (the unknowns). A system L is said to be beta-solvable (beta eta-solvable) ...
详细信息
A system of equations in the lambda-calculus is a set of formulas of lambda (the equations) together with a finite set of variables of lambda (the unknowns). A system L is said to be beta-solvable (beta eta-solvable) iff there exists a simultaneous substitution with closed lambda-terms for the unknowns that makes the equations of L theorems in the theory beta (beta eta). A system L can be viewed as a set of specifications (the equations) for a finite set of programs (the unknowns) whereas a solution for L yields executable codes for such programs. A class G of systems for which the solvability problem is effectively decidable defines an equational programming language and a system solving algorithm for G defines a compiler for such language. This leads us to consider separation-like systems (SL-systems), i.e. systems with equations having form x (M) over right arrow = z, where x is an unknown and z is a free variable which is not an unknown. We show that the beta (beta eta)-solvability problem for SL-systems is undecidable. On the other hand we are able to define a class of SL-systems (regular SL-systems) for which the beta-solvability problem is decidable in Polynomial Time. Such class yields an equational programming language in which self-application is handled, constraints on executable code to be generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way.
We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor ...
详细信息
We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus. (C) 2003 Elsevier B.V. All rights reserved.
In this paper an implicit characterization of the complexity classes k-EXPand k-FEXP, for k >= 0, is given, by a type assignment system for a stratified lambda-calculus, where types for programs are witnesses of th...
详细信息
In this paper an implicit characterization of the complexity classes k-EXPand k-FEXP, for k >= 0, is given, by a type assignment system for a stratified lambda-calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic (ELL), and the hierarchy of complexity classes k-EXP is characterized by a hierarchy of types. (C) 2018 Elsevier Inc. All rights reserved.
Dynamic binding is a runtime lookup operation which extracts values corresponding to some "names" from some "environments" (finite, unordered associations of names and values). Many situations rela...
详细信息
Dynamic binding is a runtime lookup operation which extracts values corresponding to some "names" from some "environments" (finite, unordered associations of names and values). Many situations related with flexible software assembly involve dynamic binding: first-class modules, mobile code, object-oriented message passing. This paper proposes lambda N, a compact extension of the lambda-calculus to model dynamic binding, where variables are labelled by names, and where arguments are passed to functions along named channels. The resulting formalism preserves familiar properties of the lambda-calculus, has a Curry-style-type inference system, and has a formal notion of compatibility for reasoning about extensible environments. It can encode records and record extensions, as well as first-class contexts with context-filling operations, and therefore provides a basic framework for expressing a wide range of name-based coordination mechanisms. An experimental functional language based on lambda N illustrates the exploitation of dynamic binding in programming language design.
A system of equations in the lambda-calculus is a set of formulas of lambda (the equations) together with a finite set of variables of lambda (the unknowns), A system L is said to be beta-solvable (beta eta-solvable) ...
详细信息
A system of equations in the lambda-calculus is a set of formulas of lambda (the equations) together with a finite set of variables of lambda (the unknowns), A system L is said to be beta-solvable (beta eta-solvable) iff there exists a simultaneous substitution with closed lambda-terms for the unknowns that makes the equations of L theorems in the theory beta (beta eta). A system L can be viewed as a set of specifications (the equations) for a finite set of programs (the unknowns) whereas a solution for L yields executable codes for such programs. A class G of systems for which the solvability problem is effectively decidable defines an equational programming language and a system solving algorithm for G defines a compiler for such language. This leads us to consider separation-like systems (SL-systems), i.e. systems with equations having form x (M) over right arrow = z, where x is an unknown and z is a free variable which is not an unknown. It is known that the beta (beta eta)-solvability problem for SL-systems is undecidable. Here we show that there is a class of SL-systems (NP-regular SL-systems) for which the beta-solvability problem is NP-complete. Moreover, we show that any SL-system L can be transformed into an NP-regular SL-system L'. This transformation consists of adding abstractions to the LHS occurrences of the RHS variables of L. In this sense NP-regular SL-systems isolate the source of undecidability for SL-systems, namely: a shortage of abstractions on the LHS occurrences of the RHS variables. NP-regular SL-systems yield an equational programming language in which unrestrained self-application is handled, constraints on executable code to be generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way. However, existence of executable code satisfying a specification in such language is an NP-complete problem. This is the price we have to pay for allowing unrestrained self-application in
We study an extension of Plotkin's call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus,...
详细信息
We study an extension of Plotkin's call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus, so that it enjoys elegant characterizations of many semantic properties. We prove that this extended calculus is a conservative refinement of Plotkin's one. In particular, the notions of solvability and potential valuability for this calculus coincide with those for Plotkin's call-by-value lambda-calculus. The proof rests on a standardization theorem proved by generalizing Takahashi's approach of parallel reductions to our set of reduction rules. The standardization is weak (i.e. redexes are not fully sequentialized) because of overlapping interferences between reductions.
We consider the untyped lambda-calculus with beta-reduction and algebraic rewrite rules for some constants. The rules must be left-linear and must not contain applications of variables in their left sides. We prove th...
详细信息
We consider the untyped lambda-calculus with beta-reduction and algebraic rewrite rules for some constants. The rules must be left-linear and must not contain applications of variables in their left sides. We prove that the combined reduction relation is confluent (Church-Rosser) if the algebraic rewrite system alone is confluent. This result also holds when reduction is restricted to a subset of terms with suitable closure conditions. (This subset may be a set of well-typed terms.)
We introduce an extension of lambda-calculus, called label-selective lambda-calculus, in which arguments of functions are selected by labels. The set of labels combines symbolic keywords with numeric positions. While ...
详细信息
We introduce an extension of lambda-calculus, called label-selective lambda-calculus, in which arguments of functions are selected by labels. The set of labels combines symbolic keywords with numeric positions. While the former enjoy free commutation, the latter and relative renumbering are needed to extend commutation to conflictuous names, and allow full currying. This extension of lambda-calculus is conservative, in the sense that when we restrict ourselves to using only one label, it coincides with lambda-calculus. The main result of this paper is the proof that the label-selective lambda-caculus is confluent. In other words, argument selection and reduction commute.
暂无评论