Higher-Order Types and Information Modeling

Advances in Database Research - Advanced Topics in Database Research, Volume 4 ◽

10.4018/978-1-59140-471-2.ch010 ◽

2005 ◽

pp. 218-237 ◽

Cited By ~ 4

Author(s):

Terry Halpin

Keyword(s):

Unified Modeling Language ◽

Higher Order ◽

Order Logic ◽

Information Modeling ◽

Relational Model ◽

Unified Modeling ◽

First Order ◽

Order Types ◽

Key Issues ◽

Object Role Modeling

While some information modeling approaches (e.g., the Relational Model and Object-Role Modeling) are typically formalized using first-order logic, other approaches to information modeling include support for higher-order types. There appear to be three main reasons for requiring higher-order types: (1) to permit instances of categorization types to be types themselves (e.g., the Unified Modeling Language introduced power types for this purpose); (2) to directly support quantification over sets and general concepts; (3) to specify business rules that cross levels/meta levels (or ignore level distinctions) in the same model. As the move to higher-order logic may add considerable complexity to the task of formalizing and implementing a modeling approach, it is worth investigating whether the same practical modeling objectives can be met while staying within a first-order framework. This chapter examines some key issues involved, suggests techniques for retaining a first-order formalization, and makes some suggestions for adopting a higher-order semantics.

Download Full-text

Operations with Higher-Order Types of Asymptotic Variation: Filling Some Gaps

Advances in Pure Mathematics ◽

10.4236/apm.2021.118046 ◽

2021 ◽

Vol 11 (08) ◽

pp. 687-716

Author(s):

Antonio Granata

Keyword(s):

Higher Order ◽

Order Types

Download Full-text

Sound and complete models of contracts

Journal of Functional Programming ◽

10.1017/s0956796806005971 ◽

2006 ◽

Vol 16 (4-5) ◽

pp. 375-414 ◽

Cited By ~ 34

Author(s):

MATTHIAS BLUME ◽

DAVID McALLESTER

Keyword(s):

Ad Hoc ◽

Expressive Power ◽

Higher Order ◽

Original Version ◽

Order Types ◽

Restricted Form ◽

Soundness And Completeness ◽

Recursive Contracts ◽

Intuitive Interpretation ◽

Typed Languages

Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. They did not, however, give a semantics of contracts. The lack of a semantics makes it impossible to define and prove soundness and completeness of the checking algorithm. (Given a semantics, a sound checker never reports violations that do not exist under that semantics; a complete checker is – in principle – able to find violations when violations exist.) Ideally, a semantics should capture what programmers intuitively feel is the meaning of a contract or otherwise clearly point out where intuition does not match reality. In this paper we give an interpretation of contracts for which we prove the Findler-Felleisen algorithm sound and (under reasonable assumptions) complete. While our semantics mostly matches intuition, it also exposes a problem with predicate contracts where an arguably more intuitive interpretation than ours would render the checking algorithm unsound. In our semantics we have to make use of a notion of safety (which we define in the paper) to avoid unsoundness. We are able to eliminate the “leakage” of safety into the semantics by changing the language, replacing the original version of unrestricted predicate contracts with a restricted form. The corresponding loss in expressive power can be recovered by making safety explicit as a contract. This can be done either in ad-hoc fashion or by including general recursive contracts. The addition of recursive contracts has far-reaching implications, deeply affecting the formulation of our model and requiring different techniques for proving soundness.

Download Full-text

The complexity of type inference for higher-order typed lambda calculi

Journal of Functional Programming ◽

10.1017/s0956796800001143 ◽

1994 ◽

Vol 4 (4) ◽

pp. 435-477 ◽

Cited By ~ 9

Author(s):

Fritz Henglein ◽

Harry G. Mairson

Keyword(s):

Lower Bounds ◽

Higher Order ◽

Type Inference ◽

Boolean Logic ◽

Turing Machines ◽

Technical Tool ◽

Inference Problem ◽

Exponential Time ◽

First Order ◽

Order Types

AbstractWe analyse the computational complexity of type inference for untyped λ-terms in the second-order polymorphic typed λ-calculus (F2) invented by Girard and Reynolds, as well as higher-order extensions F3, F4, …, Fω proposed by Girard. We prove that recognising the F2-typable terms requires exponential time, and for Fω the problem is non-elementary. We show as well a sequence of lower bounds on recognising the Fk-typable terms, where the bound for Fk+1 is exponentially larger than that for Fk.The lower bounds are based on generic simulation of Turing Machines, where computation is simulated at the expression and type level simultaneously. Non-accepting computations are mapped to non-normalising reduction sequences, and hence non-typable terms. The accepting computations are mapped to typable terms, where higher-order types encode reduction sequences, and first-order types encode the entire computation as a circuit, based on a unification simulation of Boolean logic. A primary technical tool in this reduction is the composition of polymorphic functions having different domains and ranges.These results are the first nontrivial lower bounds on type inference for the Girard/Reynolds system as well as its higher-order extensions. We hope that the analysis provides important combinatorial insights which will prove useful in the ultimate resolution of the complexity of the type inference problem.

Download Full-text

BIM gestützte strukturdynamische Analyse mit Volumenelementen höherer Ordnung/BIM-based structural dynamic analysis using higher-order volumetric finite elements

Bauingenieur ◽

10.37544/0005-6650-2018-04-76 ◽

2018 ◽

Vol 93 (04) ◽

pp. 160-166

Author(s):

A. Paolini ◽

F. Frischmann ◽

S. Kollmannsberger ◽

A. Rabold ◽

T. Horger ◽

...

Keyword(s):

Finite Elements ◽

Dynamic Analysis ◽

Building Information Modeling ◽

Higher Order ◽

Information Modeling ◽

Structural Dynamic ◽

Finite Elemente ◽

Building Information

Building Information Modeling ermöglicht die automatisierte Erstellung von Simulationsmodellen und schafft somit eine wichtige Grundlage, Zeit und Kosten einzusparen sowie die Qualität der Planung von Gebäuden zu erhöhen. Die Art des Simulationsmodells hängt jedoch wesentlich von der konkreten Problemstellung ab. Für Schwingungsanalysen bei Massivholzkonstruktionen ist eine mechanisch korrekte Beschreibung der Stoßstellen zwischen den Bauteilen von großer Bedeutung. Dafür eignen sich Modelle aus hexaedrischen finiten Elementen erheblich besser als Schalenelemente. Ein konformes Hexaedernetz kann allerdings mit verfügbaren Netzgeneratoren nur bei bestimmten Gebäudegeometrien automatisch erzeugt werden und weist an Stoßstellen eine große Anzahl von Elementen auf, was zu einem hohen Rechenaufwand führen kann. Im vorliegenden Beitrag wird deshalb ein alternatives Verfahren vorgestellt, mit dem ein hexaedrisches Finite-Elemente-Modell automatisch aus einem Bauwerksinformationsmodell (BIM) abgeleitet werden kann. Die im BIM definierten Bauteile werden dabei getrennt voneinander vernetzt und deren Verbindungen zueinander mithilfe der Mortar-Methode abgebildet. Eine große Recheneffizienz wird durch die Verwendung von Ansatzfunktionen höherer Ordnung in Kombination mit einem relativ groben Netz erreicht. Nach der Beschreibung des Verfahrens wird seine Anwendbarkeit an einem mehrgeschossigen Massivholzgebäude demonstriert.

Download Full-text