User vijay d - MathOverflow

Why the preimage rather than image in Stone-type dualities.

2013-01-09T23:28:18Z

I am seeking a deeper understanding of the representation of set-based objects in terms of Boolean algebras.

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.

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.

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?

Answer by Vijay D for "Duals" of Lindenbaum algebras

2011-09-17T01:09:45Z

What you have defined is one way to go about this. There is another question 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

The mathematics of metamathematics by Helena Rasiowa and Roman Sikorski.

The topic is briefly treated in the chapter on model theory in

Mathematical Logic: A Course with Exercises Pt.2: Recursion Theory, Godel's Theorem, Set Theory and Model Theory, by Rene Cori, Daniel Lascar.

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).

Algebraic logic by Hajnal Andréka, István Németi and Ildikó Sain, and the article Applying Algebraic Logic; a General Methodology by Hajnal Andréka, Ágnes Kurucz, István Németi and Ildikó Sain

Answer by Vijay D for Is there a theorem that says that there is always more than one way to "continue a finite sequence"?

2011-09-13T00:39:25Z

There is an area of computer science called grammatical inference.

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.

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.

There is a theorem due to E. Mark Gold (Language Identification in the Limit, 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.

This result may be one formalisation related to the original question, but does not tell the whole story. Dana Angluin (Inference of Reversible Languages, 1982) showed that there are families containing infinitely many languages that can be learnt in the limit. There is a recent text Grammatical Inference: Learning Automata and Grammars by Colin de la Higuera devoted to this area.

Answer by Vijay D for Algorithm to compute certain poset from a given poset.

2011-09-04T02:14:58Z

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$.

$f$ maps $X \subseteq O$ to $\{ y \in A \mid \text{for all }x \in X, (x,y) \in R \}$

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:

Algorithms for the Construction of Concept Lattices and Their Diagram Graphs, Kuznetsov, Sergei O.; Obiedkov, Sergei A. (2001)

The Formal Concept Analysis site contains links to relevant material and software.

Answer by Vijay D for What's a magical theorem in logic?

2011-08-30T10:35:12Z

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.

Answer by Vijay D for The concept of Duality

2011-08-27T00:36:37Z

This answer has a heavy bias towards logical structures. The simplest notion I know is order-theoretic duality.

The dual of an order is the inverse relation of the order (less-than vs. greater-than, subset vs. superset)
Greatest lower bounds and least upper bounds (minimum vs. maximum, intersection vs. union, conjunction vs. disjunction)
Bottom and top
Least and greatest fixed points
Additive and multiplicative maps

In structures containing negation, we have De Morgan duality, such as the examples from logic given by Joel David Hamkins.

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:

Conjunction and implication (both with one argument fixed) are adjoints
Existential and universal quantification are adjoints to a certain form of substitution
Strongest postconditions and weakest liberal preconditions in programming language semantics
Sets of models and sets of formulae
A lattice and its image under a closure operator

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.

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.

Complete, atomic, Boolean algebras and powersets [Lindenbaum and Tarski]
Finite distributive lattices and finite posets [Birkhoff]
Completely distributive, algebraic lattices and posets [Raney, others I cannot recall]
Boolean algebras with operators and sets with relations [Jónsson and Tarski]
Distributive algebras with operators and ordered sets with relations [Gehrke and Jónsson (though there may be earlier work)]

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.

Boolean algebras and Stone spaces [Stone]
Distributive lattices and Priestley spaces [Priestley]
Heyting algebras and Esakia spaces [Esakia]
Topological representations of arbitrary lattices [Urquhart]
Extensions of Stone and Priestley duality to lattices with operators
Dualities arising in Modal logic [Goldblatt]

One 'analogy between analogies' is that of a dualising object. The term schizophrenic object has also been used in this context.

Porst and Tholen's article Concrete Dualities 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.

Answer by Vijay D for Program transformation as alternative for Hoare logic or temporal logic

2011-07-21T01:32:51Z

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.

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).

Robert Keller, 1976, Formal verification of parallel programs.
Gordon Plotkin, 1981. Structural Operational Semantics.

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.

David M. R. Park, 1969, Fixpoint induction and proofs of program properties.
Lawrence Flon and Norihisa Suzuki, 1975, Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs.
Patrick Cousot and Radhia Cousot, 1977, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.

Finally, there is a precise mathematical sense in which the fixed point (or transitive closure) approach is not significantly different from Floyd/Hoare logic.

Edmund M. Clarke Jr., 1977, Program Invariants as Fixed Points.

To quote from the abstract of the paper:

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.

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.

Neil Immerman, Alexander Rabinovich, Thomas W. Reps, Mooly Sagiv, and Greta Yorsh, 2004, The Boundary Between Decidability and Undecidability for Transitive Closure Logics.

Edit: Adding a link.

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.

Answer by Vijay D for Transition Graph per alphabet?

2011-07-24T23:10:53Z

Adding a post because I lack the rep to comment.

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.

These pages may help (the latter two based on your tags).

Answer by Vijay D for What could be some potentially useful mathematical databases?

2011-06-21T23:05:58Z

There are two databases I have wished for during my studies.

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.

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.

Answer by Vijay D for the maximal length of a special dicksonian sequence

2011-05-06T06:15:27Z

I lack the rep to comment. This paper may help with the calculations.

Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma http://arxiv.org/abs/1007.2989

Answer by Vijay D for Do Turing Machines generates any nontrivial lattice on the set o symbols or states?

2011-03-07T16:14:31Z

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.

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.

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.

Comment by Vijay D

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?

Comment by Vijay D

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.

Comment by Vijay D

2013-01-10T00:12:50Z

That's what I meant by preimage being a homomorphism while image may not be one.

Comment by Vijay D

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.

Comment by Vijay D

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.

Comment by Vijay D

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.

Comment by Vijay D

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.

Comment by Vijay D

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.

Comment by Vijay D

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.

Comment by Vijay D

2011-07-25T11:10:20Z

Many. Or something to that effect.