40

A type $C$ has a logarithm to base $X$ of $P$ exactly when $C \cong P\to X$. That is, $C$ can be seen as a container of $X$ elements in positions given by $P$. Indeed, it's a matter of asking to what power $P$ we must raise $X$ to obtain $C$. It makes sense to work with $\mathop{log}F$ where $F$ is a functor, whenever the logarithm exists, meaning $\mathop{...


35

There are actually two uses of the word "strength" in play here. A strong endofunctor $F : C \to C$ over a monoidal category $(C, \otimes, I)$ is one which comes with a natural transformation $\sigma : A \otimes F(B) \to F(A \otimes B)$, satisfying some coherence conditions with respect to the associator which I will gloss over. This condition is sometimes ...


33

Consider the function (taken from here) $\qquad \displaystyle f(n) = \begin{cases} 1 & 0^n \text{ occurs in the decimal representation of } \pi \\ 0 & \text{else}\end{cases}$ Despite the looks, $f$ is computable by the following argument. Either $0^n$ occurs for every $n$ or there is a $k$ so that $0^k$ occurs but $0^{k+1}$ does not. We do not ...


29

The answer depends on $k$, $m$, and $n$. Exact counts are generally not known, but there is a "threshold" phenomenon that for most settings of $k$, $m$, $n$, either nearly all $k$-SAT instances are satisfiable, or nearly all instances are unsatisfiable. For example, when $k=3$, it has been empirically observed that when $m < 4.27 n$, all but a $o(1)$ ...


27

HoTT "suffers" from Gödel incompleteness, of course, since it has a computably enumerable language and rules of inference, and we can formalize arithmetic in it. The authors of the HoTT book were perfectly aware of its incompletness. (In fact, this is quite obvious, especially when half of the authors are logicians of some sort). But does incompleteness "...


26

This may not be exactly what you mean, but Seth Pettie and Vijaya Ramachandran's optimal minimum spanning tree algorithm is in some sense non-constructive. It is an open question whether there is a deterministic algorithm to compute minimum spanning trees in linear (meaning $O(n+m)$) time. Pettie and Ramachandran describe an algorithm that computes MSTs in ...


26

He wanted to create a formal system for the foundations of logic and mathematics that was simpler than Russell's type theory and Zermelo's set theory. The basic idea was to add a constant $\Xi$ to the untyped lambda calculus (or combinatory logic) and interpret $XZ$ as expressing "$Z$ satisfies the predicate $X$" and $\Xi XY$ as expressing "$X\subseteq Y$". ...


25

Firstly, I want to address the comments to the question, where it was suggested that "false" expresses $P = PSPACE$ because the statement is false. While this might be a good joke, it is actually very much harmful to think this way. When we ask how to express a certain sentence in a certain formal system, we are not talking about truth values. If we were, ...


24

As Steven notes, the canonical example is $\mathsf{IP} = \mathsf{PSPACE}$. This collapse does not relativize, in the sense that there is an oracle $A$, subject to which $\mathsf{IP}^A \ne \mathsf{PSPACE}^A$. The intuition why the known proof of this result avoids the relativization barrier is that it uses arithmetization (Yonatan alluded to this in a comment)...


24

Very briefly: the simply-typed $\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from propositional to first-order logic. The key contribution of Martin-Löf's is a novel analysis of equality. There are two main ways of giving Curry-Howard style ...


22

I am not aware of a paper concerned with the comparison between symbolic execution and abstract interpretation. Nor do I think one is needed. Reading the original descriptions of these two techniques should be enough. King, Symbolic Execution and Program Testing, 1976 Cousot, Cousot, Abstract Interpretation: a Unified Lattice Model for Static Analysis of ...


21

Algebraic data types let you define types recursively. Concretely, suppose we have the datatype $$ \mathsf{data\;list = Nil \;\;|\;\; Cons\;of\;\mathbb{N} \times list} $$ What this means is that $\mathsf{list}$ is the smallest set generated by the $\mathsf{Nil}$ and $\mathsf{Cons}$ operators. We can formalize this by defining the operator $F(X)$ $$ ...


21

Andrej has already explained that $P=\mathit{PSPACE}$ can be written as a $\Sigma^0_2$-sentence. Let me mention that this classification is optimal in the sense that if the statement is equivalent to a $\Pi^0_2$-sentence, then this fact does not relativize. More precisely, the set of oracles $A$ such that $P^A=\mathit{PSPACE}^A$ is definable by a $\Sigma^0_2$...


21

$S^1_2$ is a theory of bounded arithmetic, that is, a weak axiomatic theory obtained by severely restricting the schema of induction of Peano arithmetic. It is one of the theories defined by Sam Buss in his thesis, other general references include Chapter V of Hájek and Pudlák’s Metamathematics of first-order arithmetic, Krajíček’s “Bounded arithmetic, ...


20

I have an answer to this question which is possibly novel. In fact, I am still thinking through it for the last 6 months or so, and it hasn't been written about in papers yet. The general thesis is that relational reasoning principles like "logical relations", "simulations", and even "invariants" are manifestations of data abstraction or information hiding....


20

If I may, quite blatantly, advertise myself, we wrote an article about this last year Abstraction-Based Algorithm for 2QBF. I've got an implementation for qdimacs, which I can provide if you wish but from my experience, one can benefit greatly from specializing the algorithm for a particular problem. There is also an older paper A Comparative Study of 2QBF ...


19

Consider algebraic datatypes such as: data List a = Nil | Cons a (List a) The return types of each constructor in a datatype are all the same: Nil and Cons both return List a. If we allow the constructors to return different types, we have a GADT: data Empty -- this is an empty data declaration; Empty has no constructors data NonEmpty data NullableList a ...


19

No, it's not possible. Consider the following two inhabitants of the type $(A \to B) \to (A \to B)$. $$ \begin{array}{l} M = \lambda f.\;f \\ N = \lambda f.\;\lambda a.\; f\;a \end{array} $$ These are distinct $\beta$-normal forms, but cannot be distinguished by a lambda-term, since $N$ is an $\eta$-expansion of $M$, and $\eta$-expansion preserves ...


19

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive mathematician. To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc: We provide a function $f$ which ...


18

How do type classes fit in this model? The short answer is: they don't. Whenever you introduce coercions, type classes, or other mechanisms for ad-hoc polymorphism into a language, the main design issue you face is coherence. Basically, you need to ensure that typeclass resolution is deterministic, so that a well-typed program has a single ...


18

Being 4-colorable? Certainly MSO, and trivial on planar graphs. It's NP-complete for a large enough forbidden clique minor, by reduction to planar 3-colorability.


18

The basic sum-of-squares proof system, introduced under the name of Positivstellensatz refutations by Grigoriev and Vorobjov, is a “static” proof system for showing that a set of polynomial equations and inequations $$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ where $f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$, has no common solution in $\...


18

You must be careful here. You are using set-theoretic concepts (cardinal, continuum) outside set theory. There is potential for confusion. Your question can be understood in several ways. Maybe you are asking whether there can be uncountably many terms of a given type. The answer is: obviously not since there are only countably many finite strings, and ...


17

Other resources could be found referenced in Kaustuv Chaudhuri's thesis "The Focused Inverse Method for Linear Logic", and you might be interested in Roy Dyckhoff's "Contraction-Free Sequent Calculi", which is about contraction but not about linear logic. There are opportunities for efficient proof search in linear logic, but I don't think current work ...


17

First, you should know that, in general, there is not consensus about these terms and their definitions depend on the system in which one is working.Since you asked about intuitionist type theory, I'll quote Pfenning: A judgment is something we may know, that is, an object of knowledge. A judgment is evident if we in fact know it. Propositions on the ...


17

Yes, but you have to consider typed combinators. That is, you need to give $S$ and $K$ the following type schemas: $$ \begin{array}{lcl} K & : & A \to B \to A \\ S & : & (A \to B \to C) \to (A \to B) \to (A \to C) \end{array} $$ where $A, B$, and $C$ are meta-variables which can be instantiated to any concrete type at each use. Then, you ...


17

Semantically, a coercion $c : A \leq B$ is just a morphism $c : A \to B$, which gets added to the interpretation of terms at the appropriate points. The basic problem this creates is the issue of coherence: are you guaranteed that a term will have a unique meaning, given that the same term can potentially have coercions hidden in many possible places in the ...


17

TL;DR. The metamathematics of binding are subtle: they seem trivial but aren't — whether you deal with (higher-order) logics or 𝜆-calculus. They're so subtle that binding representations form an open research field, with a competition (the POPLmark challenge) some years ago. There are even jokes by people in the field about the complexity of approaches to ...


17

The two words do not refer to the same thing. Hilbert's Entscheidungsproblem was the question whether there is an algorithm that decides the universal truth of first-order logical sentences, which was answered negatively by Turing in his famous 1936 paper "On Computable Numbers, with an application to the Entscheidungsproblem". The word literally means ...


16

LCF is indeed the grand-father of all these system: Coq, Isabelle, HOLs, including the ML programming language (which we see today as OCaml, SML, also F#). Yes, I am including Coq as a member of the greater LCF family. Compared to the US-American proof assistants (notably ACL2), or the totally unrelated Mizar, Coq is culturally quite close to Isabelle and ...


Only top voted, non community-wiki answers of a minimum length are eligible