L-Fuzzy Relations in Coq

Heyting categories, a variant of Dedekind categories, and Arrow categories provide a convenient framework for expressing and reasoning about fuzzy relations and programs based on those methods. In this thesis we present an implementation of Heyting and arrow categories suitable for reasoning and program execution using Coq, an interactive theorem prover based on Higher-Order Logic (HOL) with dependent types. This implementation can be used to specify and develop correct software based on L-fuzzy relations such as fuzzy controllers. We give an overview of lattices, L-fuzzy relations, category theory and dependent type theory before describing our implementation. In addition, we provide examples of program executions based on our framework.

An Abstract Algebraic Theory of L-Fuzzy Relations for Relational Databases

Classical relational databases lack proper ways to manage certain real-world situations including imprecise or uncertain data. Fuzzy databases overcome this limitation by allowing each entry in the table to be a fuzzy set where each element of the corresponding domain is assigned a membership degree from the real interval [0…1]. But this fuzzy mechanism becomes inappropriate in modelling scenarios where data might be incomparable. Therefore, we become interested in further generalization of fuzzy database into L-fuzzy database. In such a database, the characteristic function for a fuzzy set maps to an arbitrary complete Brouwerian lattice L. From the query language perspectives, the language of fuzzy database, FSQL extends the regular Structured Query Language (SQL) by adding fuzzy specific constructions. In addition to that, L-fuzzy query language LFSQL introduces appropriate linguistic operations to define and manipulate inexact data in an L-fuzzy database. This research mainly focuses on defining the semantics of LFSQL. However, it requires an abstract algebraic theory which can be used to prove all the properties of, and operations on, L-fuzzy relations. In our study, we show that the theory of arrow categories forms a suitable framework for that. Therefore, we define the semantics of LFSQL in the abstract notion of an arrow category. In addition, we implement the operations of L-fuzzy relations in Haskell and develop a parser that translates algebraic expressions into our implementation.

L-Fuzzy Structured Query Language

Lattice valued fuzziness is more general than crispness or fuzziness based on the unit interval. In this work, we present a query language for a lattice based fuzzy database. We define a Lattice Fuzzy Structured Query Language (LFSQL) taking its membership values from an arbitrary lattice L. LFSQL can handle, manage and represent crisp values, linear ordered membership degrees and also allows membership degrees from lattices with non-comparable values. This gives richer membership degrees, and hence makes LFSQL more flexible than FSQL or SQL. In order to handle vagueness or imprecise information, every entry into an L-fuzzy database is an L-fuzzy set instead of crisp values. All of this makes LFSQL an ideal query language to handle imprecise data where some factors are non-comparable. After defining the syntax of the language formally, we provide its semantics using L-fuzzy sets and relations. The semantics can be used in future work to investigate concepts such as functional dependencies. Last but not least, we present a parser for LFSQL implemented in Haskell.

List of Employees to be involved in the extension of the Port Dalhousie and Thorold Railway

List of Employees to be involved in the extension of the Port Dalhousie and Thorold Railway (1 page, handwritten). This is signed by S.D. Woodruff, Nov. 25, 1856.

Letter of estimate sent to S.D. Woodruff for the total cost of construction and equipment of the extension of the line to Port Colborne

Letter of estimate sent to S.D. Woodruff for the total cost of construction and equipment of the extension of the line to Port Colborne [this is unsigned]. There is an envelope with this letter that suggests that it is from Mr. Shanly, Mar. 12, 1857.

Chart of estimate of cost of Port Dalhousie and Thorold Railway extension Line no. 1

Chart of estimate of cost of Port Dalhousie and Thorold Railway extension Line no. 1 signed by Mr. Shanly, Mar. 12, 1857.

Report sent to the President and Director of the Port Dalhousie and Thorold Railway stating that the location of the line extension of the railway is completed

Report sent to the President and Director of the Port Dalhousie and Thorold Railway stating that the location of the line extension of the railway is completed. The distance from Thorold Station to Port Colborne is 20 miles. The estimate provides for construction of a permanent structure across the Chippewa and Welland River. Estimates for building a first class road, culverts and bridges will be of permanent and durable masonry. This includes estimates for various station buildings such as a warehouse in Port Colborne and a warehouse in Port Dalhousie. Surveys and plans are ready and will be registered this week. This is signed by S.D. Woodruff (2 copies) [one appears to be a rough copy] (The rough copy is 5 pages, handwritten and the other copy is 6 pages, handwritten), Apr. 8, 1857.

Voucher #2 from the Engineer Department of Port Dalhousie and Thorold Railway Extension paid to Daniel Plumsteel, Dec. 31, 1856

Voucher #2 from the Engineer Department of Port Dalhousie and Thorold Railway Extension for surveys, paid to Daniel Plumsteel, Dec. 31, 1856.

Voucher #3 from the Engineer Department of Port Dalhousie and Thorold Railway Extension paid to Thomas Woods, Dec. 31, 1856

Voucher #3 from the Engineer Department of Port Dalhousie and Thorold Railway Extension for sinking test pits, paid to Thomas Woods, Dec. 31, 1856.

Voucher #5 from the Engineer Department of Port Dalhousie and Thorold Railway Extension to George Forbes for surveys, Jan. 31, 1857

Voucher #5 from the Engineer Department of Port Dalhousie and Thorold Railway Extension to George Forbes for surveys, Jan. 31, 1857.

Voucher #6 from the Engineer Department of Port Dalhousie and Thorold Railway Extension to Thomas Woods for surveys, Jan. 31, 1857

Voucher #6 from the Engineer Department of Port Dalhousie and Thorold Railway Extension to Thomas Woods for surveys, Jan. 31, 1857.

Voucher #7 from the Engineer Department of Port Dalhousie and Thorold Railway Extension to W.G. Thompson accompanied by an abstract of vouchers and summaries of account paid by W.G. Thompson for surveys, Jan. 31, 1857

Voucher #7 from the Engineer Department of Port Dalhousie and Thorold Railway Extension to W.G. Thompson accompanied by an abstract of vouchers and summaries of account paid by W.G. Thompson for surveys, Jan. 31, 1857.

Pay roll voucher #8 from the Engineer Department of Port Dalhousie and Thorold Railway Extension for surveys in the month of February, Feb. 28, 1857

Pay roll voucher #8 from the Engineer Department of Port Dalhousie and Thorold Railway Extension for surveys in the month of February, Feb. 28, 1857.

Voucher #9 from the Engineer Department of Port Dalhousie and Thorold Railway Extension to W. G. Thompson accompanied by an abstract of vouchers for surveys, Feb. 28, 1857

Voucher #9 from the Engineer Department of Port Dalhousie and Thorold Railway Extension to W. G. Thompson accompanied by an abstract of vouchers for surveys, Feb. 28, 1857

Pay roll voucher #10 from the Engineer Department of Port Dalhousie and Thorold Railway Extension for the engineer corps. , Mar. 31, 1857

Pay roll voucher #10 from the Engineer Department of Port Dalhousie and Thorold Railway Extension for the engineer corps. , Mar. 31, 1857.