# All Questions

11,575 questions
Filter by
Sorted by
Tagged with
8 views

### Why can methods like ReSuMe, Chronotron and SPAN only train single-layer spiking neural networks?

ReSuMe, Chronotron and SPAN all use STDP-like local learning rules to implement their training algorithm (though they approach the training differently, e.g. SPAN uses gradient descent via spikes ...
55 views

### What are the issues with a set-like interpretation of quantifiers in type theory?

In his answer to a question that tries to treat universal and existential quantifiers as intersections and unions of sets, Andrej Bauer says: Forget the intersections and unions. People get this idea ...
36 views

### Reduction from Sudoku to 3SAT [closed]

Consider following problem from this file You are given a $n^2 × n^2$ grid where every entry is either blank or contains a numbers from $\{1, 2,..., n^2\}$. The goal is to decided whether the ...
21 views

### Can this be formalized as a conversion rule for CoC?

Consider the Church encoding of booleans in CoC  Bool := \forall t : * . t \to t \to t \\ T := \lambda t : * . \lambda x : t . \lambda y : t . x \\ F := \lambda t : * . \lambda x: t . \lambda y : t ....
21 views

### acquaintanceship graph and six degree of separation relate to each other

The picture which will be used to draw an acquaintanceship graph. Draw the acquaintanceship graph that represents that Tom and Patricia. Tom and Hope, Tom and Sandy, Tom and Amy, Tom and Marika, Jeff ...
56 views

### What is the least compressible probability distribution? (under entropy constraint, for an expected squared error metric)

Consider a distribution $\mathcal D$ over the reals, a real parameter $H\in\mathbb R^+$, and an integer parameter $k\in\mathbb N$. The Entropy-Constrained Quantization problem asks what is the best ...
107 views

### Does such a graph exist?

In the course of my studies on graphs I sometimes use gadgets. I am trying to construct such a gadget: an edge-colored graph $G$ that has at least one properly colored spanning tree (that is, no two ...
142 views

### Type theory and fixed points of datatypes

For the purposes of this question, say that a datatype is a type constructor with one type parameter (this is sometimes called a type operator). In Haskell, we can define a fixed point ...
69 views

51 views

### Does "clean software architecture" exhibit crystaline structure? [closed]

I was thinking today about an analogy between entropy/crystal structure (in the domain of physics) and object-oriented polymorphism. Uncle Bob Martin always talks about how high-level components must ...
109 views

### Fastest Known Algorithm to Count Acyclic Orientations in a Graph

Given an undirected graph $G$, an acyclic orientation of $G$ is choice of orientation for each edge of $G$ (turning each edge into an arc) such that the resulting directed graph has no directed cycles....
66 views

48 views

### Complexity of a matrix partition problem in graphs

All graphs in this question are finite, simple, and undirected. Let $H$ be a regular graph on at least five vertices, let $v_1,v_2,\dots,v_n$ be the vertices in $H$, and let $M$ be the adjacency ...
257 views

### What is the complexity of HORN-2CNF entailment?

I know the entailment of a propositional variable in a HORN-3CNF formula is $P$-complete. I can't find any publication in which it has been shown the complexity of the same problem for HORN-2CNF ...
129 views

### Effect of HoTT/Univalence Axiom on equality between terms of inductive types?

It is well known that Univalence contradicts Axiom K, for example there are two ways $\mathbf{2} = \mathbf{2}$ may be proved using Univalence, via $\mathtt{id}_{\mathbf{2}}$ or $\mathtt{not}$. But ...
107 views

### Hardness of computing the dimension of an integral polytope?

Given a set of linear inequalities $Ax \leq b$ let $P = \text{conv}\{x \in \{0,1\}^n \mid A x \leq b \}$ be the convex hull of all binary vectors that satisfy the given inequalities. I am interested ...
346 views

### Why is the Curry-Howard isomorphism?

The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble ...
74 views

### Expressiveness of pushdown automata whose stack height sequence is unambiguous

I consider pushdown automata on an alphabet $\Sigma$, which are intuitively finite automata with a stack. Formally, a pushdown automaton $A = (Q, q_0, F, \Gamma, \Delta)$ is a finite set $Q$ of states,...