Doctor of Philosophy, Case Western Reserve University, 2005, Computing and Information Science

Formal Concept Analysis (FCA) is a powerful tool for symbolic data analysis using a mathematical structure called lattice. FCA has novel applications in areas such as data mining and information retrieval. In this thesis, we study the theory and applications of FCA. This thesis consists of three parts. The first part introduces a new notion of formal concept, called approximable concept, and connect this notion to semantic domain theory. FCA has been traditionally focused on finite contexts and finite concept lattices, therefore neglecting the full power of the theory. After a thorough investigation, we developed a new definition of concept, inspired by the ideas of partial information and successive approximation in domain theory, to provide computationally meaningful alternative. Domain theory is a branch of order theory invented by Scott for the denotational semantics of programming languages. The theoretical contribution of this part amounts to a systematic connection, in the form of a categorical equivalence, between formal concept analysis and domain theory. The second part presents a tool for automatic concept lattice layout and visualization. Concept lattices are normally represented by a list of string pairs instead of a lattice diagram. Currently, there are no standard rules for the visualization of concept lattices. We develop a tool which creates balanced and well-built lattice diagrams for finite contexts, automatically. The diagram layout of concept lattices help us understand the whole structure of concept lattices. The third part shows a method for web-menu layout design and describes a user evaluation study comparing the resulting menu layout of an existing real world web site with the one derived from our method. Most of today's web sites' menu layouts are created by the intuition of the web designers. We propose a new FCA-based semi-automatic web-menu design methodology, called FcAWN (Formal Concept Analysis for Web Navigation), to construct more (open full item for complete abstract)

Committee: Guo-Qiang Zhang (Advisor) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2023, Mathematics

As objects that appear throughout mathematics, integer-valued polynomials have been studied extensively. However, integer-valued rational functions are a much less studied generalization. We consider the set of integer-valued rational functions over an integral domain as a ring and study the ring-theoretic properties of such rings. We explore when rings of integer-valued rational functions are Bezout domains, Prufer domains, and globalized pseudovaluation domains. We completely classify when the ring of integer-valued rational functions over a valuation domain is a Prufer domain and when it is a Bezout domain. We extend the classification of when rings of integer-valued rational functions are Prufer domains. This includes a family of rings of integer-valued rational functions that are Prufer domains, as well as a family of integer-valued rational functions that are not Prufer domains. We determine that the classification of when rings of integer-valued rational functions are Prufer domains is not analogous to the interpolation domain classification of when rings of integer-valued polynomials are Prufer domains. We also show some conditions under which the ring of integer-valued rational functions is a globalized pseudovaluation domain. We also prove that even if a pseudovaluation domain has an associated valuation domain over which the ring of integer-valued rational functions is a Prufer domain, the ring of integer-valued rational functions over the pseudovaluation domain is not guaranteed to be a globalized pseudovaluation domain. Because rings of integer-valued rational functions are rings of functions, we can study their properties with respect to evaluation. These properties include the Skolem property and its generalizations, which are properties concerning when ideals are able to be distinguished using evaluation. We connect the Skolem property to the maximal spectrum of a ring of integer-valued rational functions. This is then generalized using st (open full item for complete abstract)

Committee: K. Alan Loper (Advisor); Cosmin Roman (Committee Member); Ivo Herzog (Committee Member) Subjects: Mathematics

Doctor of Philosophy (PhD), Ohio University, 2023, Electrical Engineering & Computer Science (Engineering and Technology)

This dissertation presents Zar: a formally verified compilation pipeline from discrete probabilistic programs in the conditional probabilistic guarded command language (cpGCL) to proved-correct executable samplers in the random bit model. Zar exploits the key idea that discrete probability distributions can be reduced to unbiased coin-flipping schemes. The compiler pipeline first translates cpGCL programs into choice-fix trees, an intermediate representation suitable for reduction of biased probabilistic choices. Choice-fix trees are then translated to coinductive interaction trees for execution within the random bit model. The correctness of the composed translations establishes the sampling equidistribution theorem: compiled samplers are correct with respect to the conditional weakest pre-expectation (cwp) semantics of their cpGCL source programs. Zar is implemented and fully verified in the Coq proof assistant. We extract verified samplers to OCaml and Python and empirically validate them on a number of illustrative examples. We additionally present AlgCo (Algebraic Coinductives), a practical framework for inductive reasoning over coinductive types such as conats, streams, and infinitary trees with finite branching factor, developed during the course of this work to enable convenient formal reasoning for coinductive samplers generated by Zar. The key idea is to exploit the notion of algebraic CPO from domain theory to define continuous operations over coinductive types via primitive recursion on "dense" collections of their elements, enabling a convenient strategy for reasoning about algebraic coinductives by straightforward proofs by induction. We implement the AlgCo library in Coq and demonstrate its utility by verifying a stream variant of the sieve of Eratosthenes, a regular expression library based on coinductive tries, and weakest pre-expectation semantics for potentially nonterminating sampling processes over discrete probability distributions in the r (open full item for complete abstract)

Committee: David Juedes (Advisor); James Stewart (Committee Member); Vladimir Uspenskiy (Committee Member); Jundong Liu (Committee Member); Anindya Banerjee (Committee Member); David Chelberg (Committee Member) Subjects: Computer Science