3
votes
1answer
309 views

Fundamental Problems in Mathematics that, without Computer Sciences, would not be resolved? [closed]

Could you please give examples of fundamental questions in mathematics (let us say, pure mathematics) which were resolved fundamentally by the use of computers? More precisely, are there examples that ...
22
votes
10answers
2k views

Can We Decide Whether Small Computer Programs Halt?

The undecidability of the halting problem states that there is no general procedure for deciding whether an arbitrary sufficiently complex computer program will halt or not. Are there some large $n$ ...
4
votes
0answers
198 views

About “natural proof” of Razborov and Rudich

The famous "Natural Proof" paper ,http://www.cs.umd.edu/~gasarch/BLOGPAPERS/natural.pdf , ‎of Razborov and Rudich gives a barrier for any proof that try to separate P and NP. It mainly shows that if ...
5
votes
2answers
380 views

Why is there no product type in simply typed lambda-calculus?

Consider simply typed $\lambda$-calculus that has only the unit type as primitive. We would like to encode the product and the sum types. An encoding of the product type in the untyped ...
8
votes
1answer
276 views

Categorical Semantics for Second-Order Logics

I am currently doing some work using a categorical semantics of first-order logic. The specific semantics I am using is due to Andrew Pitts, as described in: Categorical Logic, Andrew M. Pitts, ...
1
vote
0answers
98 views

Is there an easy decision algorithm for the inhabitation problem for simple types?

Consider the basic system of simple types usually known as $TA_\lambda$. One can prove that (as a consequence of the Subject Reduction Property and the fact that any typable term is strongly ...
0
votes
1answer
142 views

Interaction-based approximation for HP-complete λ-theory?

We are looking for a proof or counter-examples for the following hypothesis. Two combinators $M$ and $N$ are solvable and equivalent in the HP-complete sensible $\lambda$-theory iff either $$ \exists ...
3
votes
2answers
182 views

Smallest base to reach partial recursive functions as a closure of unbound search

It is customary to define the class of partial recursive functions by taking the set of primitive recursive functions $PR$ and taking closure over unbound search operation. Do we need the "whole" set ...
1
vote
1answer
189 views

Hypothesis: interaction-based model for λKβη

We are looking for a proof or counter-examples to the following Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ ...
2
votes
0answers
146 views

Is it possible to implement η-reduction in interaction nets?

There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. However, all the ...
1
vote
1answer
143 views

Grzegorczyk-hierarchy, growth-rate and functions with finite image

Grzegorczyk-hierarchy divides primitive recursive functions in distinct classes with respect to their growth-rate. It seems that the higher we go the hierarchy, the more tools we have to define ...
6
votes
1answer
332 views

Is equality of terms for “real” numbers with roots, logarithm, exponential, sin, cos, and other trigonometric operations decidable with a Turing-machine?

If yes, how? Also, I know you can't do it for arbitrary statements about real numbers, but that's not what I'm asking, and by "real" numbers, I mean the numbers constructible from 1, -, /, and the ...
3
votes
1answer
170 views

Various notions of Turing reduction for partial functions

If $f$ and $g$ are partial functions $\mathbb{N} \to \mathbb{N}$, define six preorder relations $f \preceq g$ as follows: $f \mathop{\preceq_{\mathrm{S}}} g$ ("$f$ is strict/Sasso reducible to $g$") ...
9
votes
0answers
241 views

Various definitions of recursion from ordinal machines

Background: I'm trying to get an intuitive understanding of α-recursion and related concepts in higher recursion theory. Once nice book is Peter Hinman's Recursion-Theoretic Hierarchies, available ...
3
votes
2answers
224 views

What categories correspond to the typed lambda calculus with parametric types?

the unadorned typed lambda calculus correspond to the closed cartesian categories, but if we add in dependent or parametric types how are they then characterised?
2
votes
0answers
295 views

Groupoid interpretation of type theory

Hello, I read the paper on groupoid interpretation of type theory by Hofmann and Streicher and I have a question. According to the authors $Tm([[\text{Set}\:[\Gamma]\: ]])$ is the same as ...
4
votes
1answer
424 views

Deciding equivalence of regular languages

Given two regular expressions $R$ and $S$ on an alphabet $\Sigma$ it is possible to decide their equivalence as follows: build two finite automata $M_R$ and $M_S$ such that $L(R) = L(M_R)$ and $L(S) ...
6
votes
1answer
398 views

Who introduced the concept of Primitive recursive functions?

I have thought that Gödel introduced the concept of Primitive recursive functions in his seminal paper "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme" (I hope I ...
1
vote
2answers
253 views

Satisfiability problem for FOL[<,R]

Let FOL[<,R] be the fragment of first-order logic enriched with two relational symbols < and R and the first-order axioms that say: < is a strict partial order and R is an irreflexive and ...
4
votes
3answers
273 views

Existential quantification over regular predicates

A regular language over an alphabet $\Sigma$ is a subset of the set of all words over $\Sigma$ that can be accepted by some finite automaton. A regular language identifies a certain property of ...
2
votes
1answer
312 views

Algorithm for satisfiability of inequalities.

I am looking for an algorithm for checking the satisfiability (with natural values) of a set of inequalities made of variables and natural numbers, for example: $u < v, u \leq z, 3 \leq v$. In ...
3
votes
2answers
309 views

Representation of μ-recursive functions

Can every μ-recursive function be defined using a single instance of the μ operator applied to a primitive recursive function? According to Wikipedia, any μ-recursive function can be expressed as the ...
2
votes
1answer
457 views

Composite finite-state machines

A finite state machine, FSM, is a box with C input/output channels, and S states, and a fixed map $f : S\times C \to S\times C\cup {0}$. If a state $(c_i,s_j)$ is mapped to the 0 element it means it ...
1
vote
2answers
424 views

Is there constructive proof of the fact that every recursive set $A \ne \varnothing$ is recursively enumerable in non-decreasing order?

Every proof I've read about this fact considers two cases: $A$ - finite and $A$ - infinite but this is undecidable problem. So, is there constructive proof?
8
votes
2answers
295 views

Reduction rules for inductive types

(I'm not sure if I should post this here rather than at Theoretical Computer Science, I've found a lot of type theory related questions on MathOverflow) I'm working in Martin-Löf type theory with ...
7
votes
2answers
834 views

Distribution of the computable numbers on the real number line

If we order all the positive computable real numbers $r_1,r_2,r_3...$ by their Kolmogorov complexity in some language $L$, then make a histogram plot of the $r_i$ on the real line, and we scale it ...
26
votes
3answers
2k views

“Simpler” statements equivalent to Con(PA) or Con(ZFC)?

Given any reasonable formal system F (e.g., Peano Arithmetic or ZFC), we all know that one can construct a Turing machine that runs forever iff F is consistent, by enumerating the theorems of F and ...
1
vote
1answer
528 views

final step(s) for a proof that a function is not primitive recursive

My function is $f:\mathbb{N} \rightarrow \mathbb{N},\ f(n)=2\uparrow ^n 3$ , the Ackermann(-Péter) function, with the second argument fixed to 3 (and "$\uparrow$" the Knuth up-arrow), which I believe ...
8
votes
5answers
408 views

Syntactically capturing complexity classes

Primitive recursive functions are syntactically constructible in the sense that from a set of "axioms" we can build every function in the set $PR$. This basicly means that we can build a machine that ...
4
votes
1answer
413 views

What fails when using call/cc as realizer of the Peirce formula

Define the axiom constants $p_{A,B}^{((A\rightarrow B)\rightarrow A)\rightarrow A}$ as realizers of the Peirce formula, and $f_A^{\bot\rightarrow A}$ as realizers of the Ex Falso Quodlibet. Then ...
5
votes
1answer
345 views

Are innermost reductions perpetual in untyped $\lambda$-calculus?

Background In the untyped lambda calculus, a term may contain many redexes, and different choices about which one to reduce may produce wildly different results (e.g. $(\lambda x.y)((\lambda ...
14
votes
7answers
1k views

Between mu- and primitive recursion

It is well known that primitive recursion is not powerful enough to express all functions, Ackermann function being probably the best known example. Now, in the logic courses (that I have had look ...
6
votes
1answer
411 views

post correspondence problem variant

Is there an algorithm which takes as input two lists of words $v_1,...,v_n$ and $w_1,...,w_n$ over an alphabet $X$ and decides if there is an infinite sequence $(k_i)$ where $1 \leq k_i \leq n$ for ...
1
vote
2answers
893 views

post correspondence problem

I have read a couple of proofs for the undecidability of the post correspondence problem, but neither reference gave a concrete example of two lists of words over a fixed alphabet such that the ...
10
votes
3answers
623 views

Complete Extensions of First Order Logic (or Language)

Lindstrom's theorem states that any extension of FOL more expressible than FOL fails to have either compactness or Lowenheim-Skolem. When I first read Lindstrom's theorem my first reaction was: "Does ...
14
votes
2answers
1k views

Structure theorems for Turing-decidable languages?

Languages decidable by weak models of computation often have certain necessary characteristics, e.g. the pumping lemma for regular languages or the pumping lemma for context-free languages. Such ...
13
votes
3answers
1k views

What is the history of the Y-combinator?

Inspired by the comments to this question, I wonder if someone can explain the history of the fixed point combinator (often called the Y combinator) in lambda calculus. Where did it first appear? ...
11
votes
6answers
1k views

Uses of bisimulation outside of computer science.

Bisimulation is one of the most important ideas of theoretical computer science. I was wondering whether bisimilarity is used/known outside of computer science/modal logic? I am aware that it ...
11
votes
2answers
443 views

What do you use categorical glueing/sconing/Freyd covers for?

In the theory of programming languages and structural proof theory, one of the handiest techniques we have available is a method called "logical relations", in which you can prove properties of ...
12
votes
2answers
1k views

Why is Kleene's notion of computability better than Banach-Mazur's?

In this post about the difference between the recursive and effective topos, Andrej Bauer said: If you are looking for a deeper explanation, then perhaps it is fair to say that the Recursive Topos ...
2
votes
2answers
747 views

Why is every finite set Diophantine?

I understand that every finite set is recursively enumerable, as I see that one could just encode each element of some finite set on a Turing Machines tape, and then have the machine check each member ...
17
votes
3answers
2k views

Satisfiability of general Boolean formulas with at most two occurrences per variable

(If you know basics in theoretical computer science, you may skip immediately to the dark box below. I thought I would try to explain my question very carefully, to maximize the number of people that ...
3
votes
2answers
758 views

computation, algebra, logic

So a really simple way of describing a digital computer is to say that it is a device for performing boolean operations. You feed it a bunch of bit strings, which is a description of the problem and ...