The expressive power of higher-order types or, life without CONS

2001 ◽  
Vol 11 (1) ◽  
pp. 55-94 ◽  
Author(s):  
NEIL D. JONES
Keyword(s):  
Programming Languages ◽  
Expressive Power ◽  
Higher Order ◽  
Second Order ◽  
Complexity Classes ◽  
Functional Program ◽  
Control Structures ◽  
First Order ◽  
Partial Recursive Functions ◽  
Turing Complete

Compare first-order functional programs with higher-order programs allowing functions as function parameters. Can the the first program class solve fewer problems than the second? The answer is no: both classes are Turing complete, meaning that they can compute all partial recursive functions. In particular, higher-order values may be first-order simulated by use of the list constructor ‘cons’ to build function closures. This paper uses complexity theory to prove some expressivity results about small programming languages that are less than Turing complete. Complexity classes of decision problems are used to characterize the expressive power of functional programming language features. An example: second-order programs are more powerful than first-order, since a function f of type [Bool]-〉Bool is computable by a cons-free first-order functional program if and only if f is in PTIME, whereas f is computable by a cons-free second-order program if and only if f is in EXPTIME. Exact characterizations are given for those problems of type [Bool]-〉Bool solvable by programs with several combinations of operations on data: presence or absence of constructors; the order of data values: 0, 1, or higher; and program control structures: general recursion, tail recursion, primitive recursion.

scholarly journals Higher-Order Illative Combinatory Logic

2013 ◽  
Vol 78 (3) ◽  
pp. 837-872 ◽  
Author(s):  
Łukasz Czajka
Keyword(s):  
Strong Consistency ◽  
Predicate Logic ◽  
Higher Order ◽  
Second Order ◽  
Model Construction ◽  
Partial Answer ◽  
Combinatory Logic ◽  
First Order ◽  
Propositional Quantifiers

AbstractWe show a model construction for a system of higher-order illative combinatory logic thus establishing its strong consistency. We also use a variant of this construction to provide a complete embedding of first-order intuitionistic predicate logic with second-order propositional quantifiers into the system of Barendregt, Bunder and Dekkers, which gives a partial answer to a question posed by these authors.

Higher-Order Multilevel Solvers for the EHL Line and Point Contact Problem

1994 ◽  
Vol 116 (4) ◽  
pp. 741-750 ◽  
Author(s):  
C. H. Venner
Keyword(s):  
Contact Problem ◽  
Computing Time ◽  
Point Contact ◽  
Higher Order ◽  
Second Order ◽  
Point Of View ◽  
First Order ◽  
Fundamental Point ◽  
Numerical Solver ◽  
Circular Contact

This paper addresses the development of efficient numerical solvers for EHL problems from a rather fundamental point of view. A work-accuracy exchange criterion is derived, that can be interpreted as setting a limit to the price paid in terms of computing time for a solution of a given accuracy. The criterion can serve as a guideline when reviewing or selecting a numerical solver and a discretization. Earlier developed multilevel solvers for the EHL line and circular contact problem are tested against this criterion. This test shows that, to satisfy the criterion a second-order accurate solver is needed for the point contact problem whereas the solver developed earlier used a first-order discretization. This situation arises more often in numerical analysis, i.e., a higher order discretization is desired when a lower order solver already exists. It is explained how in such a case the multigrid methodology provides an easy and straightforward way to obtain the desired higher order of approximation. This higher order is obtained at almost negligible extra work and without loss of stability. The approach was tested out by raising an existing first order multilevel solver for the EHL line contact problem to second order. Subsequently, it was used to obtain a second-order solver for the EHL circular contact problem. Results for both the line and circular contact problem are presented.

From First-Order Coherence to Higher-Order Coherence of Synchrotron Radiation

1998 ◽  
Vol 5 (3) ◽  
pp. 305-308 ◽  
Author(s):  
Tsuneaki Miyahara
Keyword(s):  
Synchrotron Radiation ◽  
Free Electron ◽  
Higher Order ◽  
Second Order ◽  
Free Electron Lasers ◽  
First Order ◽  
Noise Characteristics ◽  
The Difference

The difference between first-order and second-order coherence of synchrotron radiation is discussed in relation to how they can be measured and how they affect the noise characteristics of future free-electron lasers.

KK Compatibilism

2021 ◽  
pp. 40-54
Author(s):  
Mona Simion
Keyword(s):  
Higher Order ◽  
Second Order ◽  
High Stakes ◽  
Proper Action ◽  
First Order ◽  
Knowing That

According to KK Compatibilism, the unassertability in the high-stakes contextualist cases can be explained in terms of the subjects lack of higher-order knowledge: although, strictly speaking, all that is needed for proper action—assertion included—is first-order knowledge, when the stakes are high, we tend to find people who act without knowing that they meet the condition for proper action blameworthy for so doing. This chapter argues that (1) the view misidentifies the epistemic deficit that is explanatorily salient in contextualist cases, in that the absence of second-order knowledge is not a difference maker, and (2) on closer look, the account requires normative finessing for extensional adequacy.

Second-order logic, philosophical issues in

2018 ◽  
Author(s):  
Stewart Shapiro
Keyword(s):  
Mathematical Practice ◽  
Expressive Power ◽  
Deductive System ◽  
Second Order ◽  
Order Logic ◽  
Mathematical Structures ◽  
First Order ◽  
Correct Reasoning ◽  
Second Order Logic

Typically, a formal language has variables that range over a collection of objects, or domain of discourse. A language is ‘second-order’ if it has, in addition, variables that range over sets, functions, properties or relations on the domain of discourse. A language is third-order if it has variables ranging over sets of sets, or functions on relations, and so on. A language is higher-order if it is at least second-order. Second-order languages enjoy a greater expressive power than first-order languages. For example, a set S of sentences is said to be categorical if any two models satisfying S are isomorphic, that is, have the same structure. There are second-order, categorical characterizations of important mathematical structures, including the natural numbers, the real numbers and Euclidean space. It is a consequence of the Löwenheim–Skolem theorems that there is no first-order categorical characterization of any infinite structure. There are also a number of central mathematical notions, such as finitude, countability, minimal closure and well-foundedness, which can be characterized with formulas of second-order languages, but cannot be characterized in first-order languages. Some philosophers argue that second-order logic is not logic. Properties and relations are too obscure for rigorous foundational study, while sets and functions are in the purview of mathematics, not logic; logic should not have an ontology of its own. Other writers disqualify second-order logic because its consequence relation is not effective – there is no recursively enumerable, sound and complete deductive system for second-order logic. The deeper issues underlying the dispute concern the goals and purposes of logical theory. If a logic is to be a calculus, an effective canon of inference, then second-order logic is beyond the pale. If, on the other hand, one aims to codify a standard to which correct reasoning must adhere, and to characterize the descriptive and communicative abilities of informal mathematical practice, then perhaps there is room for second-order logic.

Second-Order Backward Blocking and Unovershadowing in Human Causal Learning

2002 ◽  
Vol 49 (1) ◽  
pp. 27-33 ◽  
Author(s):  
Jan De Houwer ◽  
Tom Beckers
Keyword(s):  
Higher Order ◽  
Second Order ◽  
Causal Learning ◽  
First Order ◽  
Human Causal Learning ◽  
Before And After ◽  
Causal Status

Abstract. De Houwer and Beckers (in press , Experiment 1) recently demonstrated that ratings about the relation between a target cue T2 and an outcome are higher when training involves CT1+ and T1T2+ followed by C+ trials than when training involves CT1+ and T1T2+ followed by C- trials. We replicated this study but now explicitly asked participants to rate the causal status of the cues both before and after the C+ or C- trials. Results showed that causal ratings for T2 were significantly higher after C+ trials than before C+ trials and that T2 received significantly lower ratings after C- trials than before C- trials. The results thus provide the first evidence for higher-order unovershadowing and higher-order backward blocking. In addition, the ratings for T1 revealed that first-order backward blocking (i.e., decrease in ratings for T1 as the result of C+ trials) was stronger than first-order unovershadowing (i.e., increase in ratings for T1 as the result of C- trials).

scholarly journals Conservative Transport Schemes for Spherical Geodesic Grids: High-Order Reconstructions for Forward-in-Time Schemes

2010 ◽  
Vol 138 (12) ◽  
pp. 4497-4508 ◽  
Author(s):  
William C. Skamarock ◽  
Maximo Menchaca
Keyword(s):  
Volume Transport ◽  
Higher Order ◽  
Second Order ◽  
Time Step ◽  
First Order ◽  
Order Reconstruction ◽  
Flow Test ◽  
Mesh Density ◽  
Original Scheme ◽  
Dependent Flow

Abstract The finite-volume transport scheme of Miura, for icosahedral–hexagonal meshes on the sphere, is extended by using higher-order reconstructions of the transported scalar within the formulation. The use of second- and fourth-order reconstructions, in contrast to the first-order reconstruction used in the original scheme, results in significantly more accurate solutions at a given mesh density, and better phase and amplitude error characteristics in standard transport tests. The schemes using the higher-order reconstructions also exhibit much less dependence of the solution error on the time step compared to the original formulation. The original scheme of Miura was only tested using a nondeformational time-independent flow. The deformational time-dependent flow test used to examine 2D planar transport in Blossey and Durran is adapted to the sphere, and the schemes are subjected to this test. The results largely confirm those generated using the simpler tests. The results also indicate that the scheme using the second-order reconstruction is most efficient and its use is recommended over the scheme using the first-order reconstruction. The second-order reconstruction uses the same computational stencil as the first-order reconstruction and thus does not create any additional parallelization issues.

scholarly journals First order quantifiers in monadic second order logic

2004 ◽  
Vol 69 (1) ◽  
pp. 118-136 ◽  
Author(s):  
H. Jerome Keisler ◽  
Wafik Boulos Lotfallah
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
Existential Quantifier ◽  
Reachability Problem ◽  
Open Problems ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic ◽  
Quantifier Alternation

AbstractThis paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01].We introduce an operation existsn (S) on properties S that says “there are n components having S”. We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a corollary, if the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict.We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W.We introduce another operation alt(S) on properties which has the same relationship with the Circuit Value Problem as reach(S) (defined in [JM01]) has with the Directed Reachability Problem. We use alt(S) to show that Πn ⊈ FO(Σn), Σn ⊈ FO(∆n). and ∆n+1 ⊈ FOB(Σn), solving some open problems raised in [Mat98].

scholarly journals Moving breathers and breather-to-soliton conversions for the Hirota equation

2015 ◽  
Vol 471 (2180) ◽  
pp. 20150130 ◽  
Author(s):  
A. Chowdury ◽  
A. Ankiewicz ◽  
N. Akhmediev
Keyword(s):  
Schrodinger Equation ◽  
Higher Order ◽  
Nonlinear Schrodinger Equation ◽  
Second Order ◽  
Periodic Oscillations ◽  
Hirota Equation ◽  
First Order ◽  
Special Values ◽  
Analytic Expression ◽  
Free Parameters

We find that the Hirota equation admits breather-to-soliton conversion at special values of the solution eigenvalues. This occurs for the first-order, as well as higher orders, of breather solutions. An analytic expression for the condition of the transformation is given and several examples of transformations are presented. The values of these special eigenvalues depend on two free parameters that are present in the Hirota equation. We also find that higher order breathers generally have complicated quasi-periodic oscillations along the direction of propagation. Various breather solutions are considered, including the particular case of second-order breathers of the nonlinear Schrödinger equation.

scholarly journals In situremoval of carbon contamination from a chromium-coated mirror: ideal optics to suppress higher-order harmonics in the carbonK-edge region

2015 ◽  
Vol 22 (6) ◽  
pp. 1359-1363 ◽  
Author(s):  
Akio Toyoshima ◽  
Takashi Kikuchi ◽  
Hirokazu Tanaka ◽  
Kazuhiko Mase ◽  
Kenta Amemiya
Keyword(s):  
Synchrotron Radiation ◽  
Vacuum Ultraviolet ◽  
Higher Order ◽  
Second Order ◽  
Edge Region ◽  
Carbon Contamination ◽  
X Ray ◽  
Photon Factory ◽  
First Order ◽  
Edge Absorption

Carbon-free chromium-coated optics are ideal in the carbonK-edge region (280–330 eV) because the reflectivity of first-order light is larger than that of gold-coated optics while the second-order harmonics (560–660 eV) are significantly suppressed by chromiumL-edge and oxygenK-edge absorption. Here, chromium-, gold- and nickel-coated mirrors have been adopted in the vacuum ultraviolet and soft X-ray branch beamline BL-13B at the Photon Factory in Tsukuba, Japan. Carbon contamination on the chromium-coated mirror was almost completely removed by exposure to oxygen at a pressure of 8 × 10−2 Pa for 1 h under irradiation of non-monochromated synchrotron radiation. The pressure in the chamber recovered to the order of 10−7 Pa within a few hours. The reflectivity of the chromium-coated mirror of the second-order harmonics in the carbonK-edge region (560–660 eV) was found to be a factor of 0.1–0.48 smaller than that of the gold-coated mirror.

Sign in / Sign up

Export Citation Format

Share Document