User vijay d - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-26T06:16:25Z http://mathoverflow.net/feeds/user/13475 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/118486/why-the-preimage-rather-than-image-in-stone-type-dualities Why the preimage rather than image in Stone-type dualities. Vijay D 2013-01-09T23:28:18Z 2013-01-10T14:05:40Z <p>I am seeking a deeper understanding of the representation of set-based objects in terms of Boolean algebras.</p> <p>Let $\wp(A)$ be the set of subsets of a set $A$. A relation $R \subseteq A \times B$ generates two operators $pre: \wp(B) \to \wp(A)$ and $post: \wp(A) \to \wp(B)$ where $pre$ maps a set $X \subseteq A$ to its preimage with respect to $R$ and $post$ maps $X$ to its image.</p> <p>In the standard Stone duality between the category of sets and Boolean algebras, a function is represented using the preimage operator. The preimage operator generated by a function turns out to be a Boolean algebra homomorphism but the image operator may not be a homomorphism. I see this as one reason to choose the preimage to represent a function. My first question is: Are there other reasons to choose the preimage representation? I feel like there should be something deeper going on. </p> <p>If we leave the setting of functions, the preimage operator generated by a relation isn't necessarily a Boolean algebra homomorphism. So, in the representation of a system of relations over a set by a Boolean algebra with operators (in the sense of Jonsson and Tarski) I see no specific motivation for using the preimage, as opposed to image operator. I see why we want to be consistent in convention, and also use the preimage because of its connection to the semantics of modal logic. However, this appears to be an aesthetic choice. My second question is: Is there a specific reason to choose the preimage, rather than image operator, when representing relations as Boolean algebras with operators?</p> http://mathoverflow.net/questions/75646/duals-of-lindenbaum-algebras/75654#75654 Answer by Vijay D for "Duals" of Lindenbaum algebras Vijay D 2011-09-17T01:09:45Z 2011-09-17T01:09:45Z <p>What you have defined is one way to go about this. There is <a href="http://mathoverflow.net/questions/65851/lindenbaum-algebras-and-models" rel="nofollow">another question</a> discussing Lindenbaum algebras and the answer by Andreas Blass discusses another possibility. Briefly, another possibility is to define an algebra over arbitrary formulas, including those containing free variables. Some people call this the Rasiowa-Sikorski approach. It is covered the the second half of the book</p> <blockquote> <p><em>The mathematics of metamathematics</em> by Helena Rasiowa and Roman Sikorski.</p> </blockquote> <p>The topic is briefly treated in the chapter on model theory in</p> <blockquote> <p><em>Mathematical Logic: A Course with Exercises Pt.2: Recursion Theory, Godel's Theorem, Set Theory and Model Theory</em>, by Rene Cori, Daniel Lascar.</p> </blockquote> <p>A tutorial style treatment that discusses some design decisions one can take in setting up an algebraic framework for studying logics is in these two articles (part 2 of the second).</p> <blockquote> <p><em><a href="http://www.math-inst.hu/pub/algebraic-logic/handbook.pdf" rel="nofollow">Algebraic logic</a></em> by Hajnal Andréka, István Németi and Ildikó Sain, and the article <em><a href="http://www.math-inst.hu/pub/algebraic-logic/meth.pdf" rel="nofollow">Applying Algebraic Logic; a General Methodology</a></em> by Hajnal Andréka, Ágnes Kurucz, István Németi and Ildikó Sain </p> </blockquote> http://mathoverflow.net/questions/4442/is-there-a-theorem-that-says-that-there-is-always-more-than-one-way-to-continue/75264#75264 Answer by Vijay D for Is there a theorem that says that there is always more than one way to "continue a finite sequence"? Vijay D 2011-09-13T00:39:25Z 2011-09-13T00:39:25Z <p>There is an area of computer science called grammatical inference.</p> <p>Let $\Sigma$ be a finite alphabet, $\Sigma^*$ be the set of finite length strings over $\Sigma$ and a language be a set of strings. Let $F$ be a family of languages. The data for the problem is a sequence of words $w_0, w_1, \ldots$ from a language in $F$. A learner receives the data and generates a sequence of languages $H_0, H_1, \ldots$ called hypotheses. </p> <p>Typically the hypothesis $H_i$ includes all words provided till that point. The learner stabilizes if the hypotheses do not change after a point and is successful if the stable hypothesis is the language from which the words were drawn. A family of languages can be learnt in the limit if there is an algorithm that can successfully learn the source language. </p> <p>There is a theorem due to E. Mark Gold (<em>Language Identification in the Limit</em>, 1967) stating that if the family $F$ contains all languages of finite cardinality and at least one language of infinite cardinality, it cannot be learnt in the limit. </p> <p>This result may be one formalisation related to the original question, but does not tell the whole story. Dana Angluin (<em>Inference of Reversible Languages</em>, 1982) showed that there are families containing infinitely many languages that can be learnt in the limit. There is a recent text <em>Grammatical Inference: Learning Automata and Grammars</em> by Colin de la Higuera devoted to this area.</p> http://mathoverflow.net/questions/74359/algorithm-to-compute-certain-poset-from-a-given-poset/74476#74476 Answer by Vijay D for Algorithm to compute certain poset from a given poset. Vijay D 2011-09-04T02:14:58Z 2011-09-04T02:14:58Z <p>I cannot tell if this will help, but mention it just in case. The area of formal concept analysis deals with algorithms for constructing lattices from sets of objects and attributes. A concept is a tuple $C = (O, A, R)$, where $O$ and $A$ are sets and $R$ is a binary relation from $O$ to $A$. The relation gives rise to a standard function $f$ from the powerset of $O$ to the powerset of $A$.</p> <p>$f$ maps $X \subseteq O$ to $\{ y \in A \mid \text{for all }x \in X, (x,y) \in R \}$</p> <p>A function $g$ from the powerset of $A$ to powerset of $O$ is similarly defined such that $f$ and $g$ form a Galois connection. The concept lattice consists of the Galois stable subsets of $A$. By choosing the relation $R$, one can generate lattices with various properties. Algorithms for lattice construction are surveyed in:</p> <p><a href="http://www.springerlink.com/content/v431je43v81nlvn8/" rel="nofollow">Algorithms for the Construction of Concept Lattices and Their Diagram Graphs</a>, Kuznetsov, Sergei O.; Obiedkov, Sergei A. (2001)</p> <p>The <a href="http://www.upriss.org.uk/fca/fca.html" rel="nofollow">Formal Concept Analysis</a> site contains links to relevant material and software.</p> http://mathoverflow.net/questions/74014/whats-a-magical-theorem-in-logic/74052#74052 Answer by Vijay D for What's a magical theorem in logic? Vijay D 2011-08-30T10:35:12Z 2011-08-30T10:35:12Z <p>The fundamental theorem of Ehrenfeucht-Fraisse games. It seems innocuous (because of the game formulation?) but the applications never stop. It provides a natural way to prove a property is not expressible in a logic. It is one of the tools of classical model theory that is also used in finite model theory. In the related notions of bisimulation and simulation, we have a cornerstone concept of concurrency theory and program verification.</p> http://mathoverflow.net/questions/73711/the-concept-of-duality/73813#73813 Answer by Vijay D for The concept of Duality Vijay D 2011-08-27T00:36:37Z 2011-08-30T10:22:14Z <p>This answer has a heavy bias towards logical structures. The simplest notion I know is order-theoretic duality.</p> <ol> <li>The dual of an order is the inverse relation of the order (less-than vs. greater-than, subset vs. superset)</li> <li>Greatest lower bounds and least upper bounds (minimum vs. maximum, intersection vs. union, conjunction vs. disjunction)</li> <li>Bottom and top </li> <li>Least and greatest fixed points</li> <li>Additive and multiplicative maps</li> </ol> <p>In structures containing negation, we have De Morgan duality, such as the examples from logic given by Joel David Hamkins. </p> <p>I do not know if 'duality' is the right term, but I think of adjunctions as duals too. To add to the answer of David Roberts:</p> <ol> <li>Conjunction and implication (both with one argument fixed) are adjoints</li> <li>Existential and universal quantification are adjoints to a certain form of substitution</li> <li>Strongest postconditions and weakest liberal preconditions in programming language semantics</li> <li>Sets of models and sets of formulae</li> <li>A lattice and its image under a closure operator</li> </ol> <p>In settings with a notion of time, there are temporal dualities from the interaction of the past and the future. There are several examples in temporal and modal logics. </p> <p>Some representation theorems for lattices are ancestors of dualities. For example, Stone's representation theorem for Boolean algebras is now usually referred to as a duality. There are various dualities relating families of lattices with families of discrete structures.</p> <ol> <li>Complete, atomic, Boolean algebras and powersets [Lindenbaum and Tarski]</li> <li>Finite distributive lattices and finite posets [Birkhoff]</li> <li>Completely distributive, algebraic lattices and posets [Raney, others I cannot recall]</li> <li>Boolean algebras with operators and sets with relations [Jónsson and Tarski]</li> <li>Distributive algebras with operators and ordered sets with relations [Gehrke and Jónsson (though there may be earlier work)]</li> </ol> <p>The list goes on. Such results are sometimes called discrete dualities. There is much recent work on discrete duality in terms of what are called canonical extensions. These duality results often include a topological component. </p> <ol> <li>Boolean algebras and Stone spaces [Stone]</li> <li>Distributive lattices and Priestley spaces [Priestley]</li> <li>Heyting algebras and Esakia spaces [Esakia]</li> <li>Topological representations of arbitrary lattices [Urquhart]</li> <li>Extensions of Stone and Priestley duality to lattices with operators</li> <li>Dualities arising in Modal logic [Goldblatt]</li> </ol> <p>One 'analogy between analogies' is that of a <a href="http://ncatlab.org/nlab/show/dualizing+object" rel="nofollow">dualising object</a>. The term schizophrenic object has also been used in this context.</p> <p>Porst and Tholen's article <a href="http://www.heldermann.de/R&amp;E/RAE18/ctw07.pdf" rel="nofollow">Concrete Dualities</a> discusses some of these and other dualities and the connection to adjunctions. Other references are Peter Johnstone's book Stone Spaces and Clarke and Davey's book Natural Dualities for the Working Algebraist.</p> http://mathoverflow.net/questions/69914/program-transformation-as-alternative-for-hoare-logic-or-temporal-logic/70869#70869 Answer by Vijay D for Program transformation as alternative for Hoare logic or temporal logic Vijay D 2011-07-21T01:32:51Z 2011-08-01T23:11:24Z <p>It appears to me that the gist of your suggestion is to translate a program into a relation and reason about the transitive closure of that relation. It is orthogonal that this relation is definable in first order arithmetic. </p> <p>The idea of translating a program into a relation is rather old and I doubt there is a unique reference for it. I will share what I know, but in each case, there are surely older papers. The first paper below suggests modelling programs as transition systems and reasoning about them. Plotkin's paper provides a way to inductively derive a transition system from program text (though the idea is much older, I'm sure).</p> <ol> <li>Robert Keller, 1976, <em>Formal verification of parallel programs</em>. </li> <li>Gordon Plotkin, 1981. <em>Structural Operational Semantics.</em> </li> </ol> <p>The transition system is essentially the relation you describe. The transitive closure is a fixed point over this relation. It is one of several objects that can be defined by fixed points. Reasoning about properties of programs using fixed points is very old too.</p> <ol> <li>David M. R. Park, 1969, <em>Fixpoint induction and proofs of program properties</em>. </li> <li>Lawrence Flon and Norihisa Suzuki, 1975, <em>Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs</em>.</li> <li>Patrick Cousot and Radhia Cousot, 1977, <em>Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints</em>.</li> </ol> <p>Finally, there is a precise mathematical sense in which the fixed point (or transitive closure) approach is not significantly different from Floyd/Hoare logic. </p> <ol> <li>Edmund M. Clarke Jr., 1977, <em>Program Invariants as Fixed Points</em>.</li> </ol> <p>To quote from the abstract of the paper:</p> <blockquote> <p>We argue that soundness and relative completeness theorems for Floyd-Hoare Axiom Systems ([3], [5], [18]) are really fixedpoint theorems. We give a characterization of program invariants as fixedpoints of functionals which may be obtained in a natural manner from the text of a program. We show that within the framework of this fixedpoint theory, soundness and relative completeness results have a particularly simple interpretation. Completeness of a Floyd-Hoare Axiom System is equivalent to the existence of a fixedpoint for an appropriate functional, and soundness follows from the maximality of this fixedpoint. </p> </blockquote> <p>Reasoning about programs by computing fixed points is extremely standard in practice. Rather than relations, we tend to deal with a transformer defined by a relation, such as a predicate or state transformer. If you are genuinely committed to reasoning over relations in a logic, you will require transitive closure logics because properties like graph reachability are not first order definable. I can point to this recent paper, but you will have to dig around for older ones.</p> <ol> <li>Neil Immerman, Alexander Rabinovich, Thomas W. Reps, Mooly Sagiv, and Greta Yorsh, 2004, <em>The Boundary Between Decidability and Undecidability for Transitive Closure Logics</em>.</li> </ol> <p>Edit: Adding a link.</p> <p>You might want to try the following verifiers that use a combination of automated reasoning and fixed point techniques. Though they may fail on harder examples, they can still discover useful invariants and errors.</p> <ol> <li><a href="http://pop-art.inrialpes.fr/interproc/interprocweb.cgi" rel="nofollow">Interproc</a></li> <li><a href="http://www.pexforfun.com/Default.aspx?language=CSharp&amp;sample=AbsVerified" rel="nofollow">Pex</a></li> </ol> http://mathoverflow.net/questions/71158/transition-graph-per-alphabet/71160#71160 Answer by Vijay D for Transition Graph per alphabet? Vijay D 2011-07-24T23:10:53Z 2011-07-24T23:10:53Z <p>Adding a post because I lack the rep to comment. </p> <p>There is at least one graph per language (assuming a language is a finite or countably infinite set of finite-length words). There will in fact be infinitely many graphs per language. You need to restrict the question further to have interesting answers. Your first question is about the graphs over a given alphabet whereas the comment later is about graphs per language. There are markedly different. </p> <p><a href="http://en.wikipedia.org/wiki/Automata_theory" rel="nofollow">These</a> <a href="http://en.wikipedia.org/wiki/Computational_number_theory" rel="nofollow">pages</a> <a href="http://en.wikipedia.org/wiki/Graph_theory" rel="nofollow">may</a> help (the latter two based on your tags).</p> http://mathoverflow.net/questions/68442/what-could-be-some-potentially-useful-mathematical-databases/68450#68450 Answer by Vijay D for What could be some potentially useful mathematical databases? Vijay D 2011-06-21T23:05:58Z 2011-06-21T23:05:58Z <p>There are two databases I have wished for during my studies. </p> <p>One of notation for various mathematical concepts, covering cultural differences. For example the different ways to denote the open-closed interval, or that different symbols are used for strict subset. LaTeX symbols or macros when they exist, would also be useful. This would have greatly helped me when reading things for the first time and later with writing. Such material is definitely out of scope for Wikipedia. </p> <p>Another useful database would be of logics and logical theories. These could range from propositional logics to higher order and infinitary logics. The theories should include various fragments of arithmetic, algebraic theories, theories of strings, etc. For each, I would be interested in what is known about decidability (and computational complexity), completeness, interpolation, etc. Currently, I use the Stanford Encyclopaedia of Philosophy and Wikipedia but what I want may often not be there or not succinctly presented for reference purposes.</p> http://mathoverflow.net/questions/64084/the-maximal-length-of-a-special-dicksonian-sequence/64090#64090 Answer by Vijay D for the maximal length of a special dicksonian sequence Vijay D 2011-05-06T06:15:27Z 2011-05-06T06:15:27Z <p>I lack the rep to comment. This paper may help with the calculations.</p> <p>Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma <a href="http://arxiv.org/abs/1007.2989" rel="nofollow">http://arxiv.org/abs/1007.2989</a></p> http://mathoverflow.net/questions/57675/do-turing-machines-generates-any-nontrivial-lattice-on-the-set-o-symbols-or-state/57688#57688 Answer by Vijay D for Do Turing Machines generates any nontrivial lattice on the set o symbols or states? Vijay D 2011-03-07T16:14:31Z 2011-03-08T17:08:57Z <p>This reply only addresses part of what you ask. Asking these questions for finite automata may be illustrative. Given an automaton (Q,L,T,q, F) with states Q, alphabet set L, transition relation T, initial state q and final states F, one can ask if (Q,T) is a partial order. In general, the answer is no. If you want to order states based on transitions, one can ask if the (reflexive) transitive closure is a partial order.</p> <p>It appears that you are asking about transition systems generated by an abstract machine. For pushdown automata and Turing machines, transitions are defined between configurations of the device. For the lambda calculus, transitions can be similarly defined. The operational semantics of an abstract machine defines the transition system it generates. Denotational semantics has a more order theoretic flavour.</p> <p>Edit:(added later) It is common to study abstract machines using lattices. Instead of states, one uses the powerset of states. The transition relation gives rise to predecessor and successor operations on this lattice. Languages, transition graphs, transition sequences, both finite and infinite can be uniformly defined as fixed points of functions on such lattices. Fixed point characterisations open the door to order-theoretic analysis and are also the basis for many practical analysis methods in programming language and applied logic research. </p> http://mathoverflow.net/questions/118486/why-the-preimage-rather-than-image-in-stone-type-dualities/118487#118487 Comment by Vijay D Vijay D 2013-01-10T03:02:56Z 2013-01-10T03:02:56Z That comment answers it. It's the insight I was looking for. Thanks! Could you add that to your answer, as answering my second question? http://mathoverflow.net/questions/118486/why-the-preimage-rather-than-image-in-stone-type-dualities/118487#118487 Comment by Vijay D Vijay D 2013-01-10T00:15:08Z 2013-01-10T00:15:08Z I see the homomorphism reason. I was wondering if there are other reasons. Also, the choice of preimage for functions does not seem to justify that choice for relations. http://mathoverflow.net/questions/118486/why-the-preimage-rather-than-image-in-stone-type-dualities Comment by Vijay D Vijay D 2013-01-10T00:12:50Z 2013-01-10T00:12:50Z That's what I meant by preimage being a homomorphism while image may not be one. http://mathoverflow.net/questions/76558/formal-verification-in-complexity-theory/76560#76560 Comment by Vijay D Vijay D 2011-09-27T23:34:14Z 2011-09-27T23:34:14Z One other large class of theorems that have been formalised are those concerning hardware and software implementations. These include statements about data-structures, algorithms, processor architectures and the like. People do get paid for such formalisations, because finding a bug in a processor has great financial value. However, a professional mathematician (or computer scientist) would probably not call these statements theorems. http://mathoverflow.net/questions/69914/program-transformation-as-alternative-for-hoare-logic-or-temporal-logic/70869#70869 Comment by Vijay D Vijay D 2011-08-07T01:40:00Z 2011-08-07T01:40:00Z Hello Lukas. Finding machine-amenable reasoning methods my research area. The methods I describe are not only foundational but also incorporated in state-of-the-art, industrial verifiers. The demos I linked to prove simple properties but that's still way more than one can achieve from scratch. Try Sumit Gulwani and Ashish Tiwari's paper on 'Combining Abstract Interpreters' for recent work on combining reasoning in theories. Thinking of fixed points as HOL is misleading because only minimal second-order reasoning is required. http://mathoverflow.net/questions/69914/program-transformation-as-alternative-for-hoare-logic-or-temporal-logic/70869#70869 Comment by Vijay D Vijay D 2011-08-04T22:58:50Z 2011-08-04T22:58:50Z The difference between FOL and FOLTC (transitive closure) is vast. Monadic Second Order logic (MSOL) has many properties that suffices to reason about properties of programs. There are many cases where R* is not computable but for a fixed Q, R*(Q) is. This difference is significant in practice. http://mathoverflow.net/questions/69914/program-transformation-as-alternative-for-hoare-logic-or-temporal-logic/70869#70869 Comment by Vijay D Vijay D 2011-08-01T23:20:28Z 2011-08-01T23:20:28Z That depends on how one encodes the fixed point. Do you want R*, the transitive closure of a relation, or R*(Init), the image of some initial predicate under R*? The latter can be encoded in the mu-calculus, which is related to monadic second order logic. The propositional mu-calculus has the finite model property, tree model property, etc. The monadic restriction buys a lot. There are many tools that compute such fixed points, including industrial grade ones that combine fixed points with a weak arithmetic theory. http://mathoverflow.net/questions/69914/program-transformation-as-alternative-for-hoare-logic-or-temporal-logic/70869#70869 Comment by Vijay D Vijay D 2011-08-01T23:04:09Z 2011-08-01T23:04:09Z Hello Lukas. Just to clarify, I'm talking about machine-generated proofs of program correctness, as opposed to machine-checked proofs. I agree that humans need not confront the gory details of a machine generated proof. Nonetheless, we don't usually want to know a program is correct, we often want some information why, such as invariants. Also, computational complexity and ease of implementation are important concerns in developing a program verifier. I do not know about the ease of implementing a Goedel numbering based verifier. Fixed-point and graph-based methods work well for simple cases. http://mathoverflow.net/questions/69914/program-transformation-as-alternative-for-hoare-logic-or-temporal-logic/70869#70869 Comment by Vijay D Vijay D 2011-08-01T00:07:55Z 2011-08-01T00:07:55Z I'm glad if you found it useful. One should distinguish between a reasoning technique that is sufficient in purely logical terms, one that humans can use, and one that machines can use. I personally think using Goedel numbers is sufficient only in purely logical terms. Various techniques works for humans and machines. Fixed points in particular fit well to automated techniques. The axiom of closure is a special instance of fixed point induction and in that form is widely used in practice. http://mathoverflow.net/questions/71158/transition-graph-per-alphabet/71160#71160 Comment by Vijay D Vijay D 2011-07-25T11:10:20Z 2011-07-25T11:10:20Z Many. Or something to that effect.