Engineering Commons^™

Intersection Type Systems And Logics Related To The Meyer-Routley System B+, Martin W. Bunder

Faculty of Engineering and Information Sciences - Papers: Part A

Some, but not all, closed terms of the lambda calculus have types; these types are exactly the theorems of intuitionistic implicational logic. An extension of these simple (→) types to intersection (or →∧) types allows all closed lambda terms to have types. The corresponding →∧ logic, related to the Meyer–Routley minimal logic B+ (without ∨), is weaker than the →∧ fragment of intuitionistic logic. In this paper we provide an introduction to the above work and also determine the →∧ logics that correspond to certain interesting subsystems of the full →∧ type theory.

Issues For Connection Of Distributed Generation In Rural/Remote Power Systems, Kashem M. Muttaqi, Gerard Ledwich, Michael Negnevitsky

Faculty of Engineering and Information Sciences - Papers: Part A

Connection of distributed generation (DG) into a distribution grid system affects the normal operation, control and protection of the distribution system. This paper addresses some of the technical issues arisen due to the addition of generation to a rural/remote distribution network. In this paper, a voltage controlled rotary DG is modelled to operate in the line of voltage sensitivity for maximum voltage improvement. A scenario-based study on DG operation and control has been conducted and recommendations for effective operation of DG presented. An investigation on barriers to inclusion of utility owned and customer owned DG has been carried out and …

Product Systems Over Right-Angled Artin Semigroups, Neal J. Fowler, Aidan Sims

Faculty of Engineering and Information Sciences - Papers: Part A

We build upon MacLane's definition of a tensor category to introduce the concept of a product system that takes values in a tensor groupoid G. We show that the existing notions of product systems fit into our categorical framework, as do the k-graphs of Kumjian and Pask. We then specialize to product systems over right-angled Artin semigroups; these are semigroups that interpolate between free semigroups and free abelian semigroups. For such a semigroup we characterize all product systems which take values in a given tensor groupoid G. In particular, we obtain necessary and sufficient conditions under which a collection of …

A Classification Of Intersection Type Systems, Martin W. Bunder

Faculty of Engineering and Information Sciences - Papers: Part A

The first system of intersection types. Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules ((ΛI ) and (ΛE) ) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction.

Urzyczyn proved in [6] that for both these systems it is undecidable whether a given intersection type is empty. Kurata and Takahashi however have shown in [5] …

Pure Type Systems With More Liberal Rules, Martin W. Bunder, Wil Dekkers

Faculty of Engineering and Information Sciences - Papers: Part A

Pure Type Systems. PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic.

First we consider a simplification of the start and weakening rules of PTSs. which allows contexts to be sets of statements, and …

Convergence Of Eigenvalues In State-Discretization Of Linear Stochastic Systems, Jose A. De Dona, Graham C. Goodwin, Richard H. Middleton, Iain Raeburn

Faculty of Engineering and Information Sciences - Papers: Part A

The transition operator that describes the time evolution of the state probability distribution for continuous-state linear systems is given by an integral operator. A state-discretization approach is proposed, which consists of a finite rank approximation of this integral operator. As a result of the state-discretization procedure, a Markov chain is obtained, in which case the transition operator is represented by a transition matrix. Spectral properties of the integral operator for the continuous-state case are presented. The relationships between the integral operator and the finite rank approximation are explored. In particular, the limiting properties of the eigenvalues of the transition matrices …

Completeness Of Two Systems Of Illative Combinatory Logic For First-Order Propositional And Predicate Calculus, Wil Dekkers, Martin Bunder, Henk Barendregt

Faculty of Engineering and Information Sciences - Papers: Part A

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus.

Systems Of Illative Combinatory Logic Complete For First Order Propositional And Predicate Calculus, Henk Barendregt, Martin Bunder, Wil Dekkers

Faculty of Engineering and Information Sciences - Papers: Part A

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the …