Martin Berger
  • Member for 9 years, 4 months
  • Last seen more than a week ago
Why is deep learning hyped despite bad VC dimension?
Accepted answer
93 votes

"If the map and the terrain disagree, trust the terrain." It's not really understood why deep learning works as well as it does, but certainly old concepts from learning theory such as VC ...

View answer
How is algorithm complexity modeled for functional languages?
34 votes

If you assume that the $\lambda$-calculus is a good model of functional programming languages, then one may think: the $\lambda$-calculus has a seemingly simple notion of time-complexity: just count ...

View answer
Is Category Theory useful for learning functional programming?
34 votes

Echoing @AJed advice, I recommend to turn your statement I want to learn category theory so I can become better at Haskell. on its head: learn Haskell, building on your programming intuition. Once ...

View answer
What does 'true concurrency' mean?
Accepted answer
25 votes

The term "true concurrency" arises in the theoretical study of concurrent and parallel computation. It is in contrast to interleaving concurrency. True concurrency is concurrency that cannot be ...

View answer
What do we gain by having "dependent types"?
Accepted answer
23 votes

Expanding my comment: Dependent types can type more programs. "More" simply means that the set of programs typable with dependent types is a proper superset of the programs typable in the simply-typed ...

View answer
Why do compilers produce assembly code?
Accepted answer
21 votes

Other reason for compilers to produce assembly rather than proper machine code are: The symbolic addresses used by assemblers instead of hard-coding machine addresses make code relocation much ...

View answer
Intro to Martin-Löf type theory
17 votes

Maybe a better question for somebody coming from set theory and grappling with how set theory and Martin-Löf type theory differ, is to reflect on what sets are. Your intuitions about set theory and ...

View answer
Universes in dependent type theory
Accepted answer
16 votes

The question under what circumstances we need to jump from a universe to one higher in the hierarchy is a good one. Having the hierarchy and the ability to climb it is important. You need to jump ...

View answer
Reference request: Category theory as it applies to type systems
Accepted answer
15 votes

Category theory is not necessary to understand programming languages, it's not even necessary to do advanced research on programming languages. Most programming language people don't know (much) ...

View answer
Lambda calculus: difference between contexts and evaluation contexts
15 votes

Context are used for many purposes, but typically to define congruences on programs. Evaluation contexts are a subset of contexts. They are typically used to define reduction relations. Let me give an ...

View answer
Deterministic SAT solver
14 votes

Core algorithms like DPLL and its refinements like CDCL are completely deterministic. Note that non-determinism doesn't necessarily mean that an algorithm may lead to a wrong result. For example we ...

View answer
Why separate lexing and parsing?
Accepted answer
14 votes

You don't have to separate them. People combine them into scannerless parsers. The key disadvantage of scannerless parsers appears to be that the resulting grammars are rather complicated -- more ...

View answer
What questions can denotational semantics answer that operational semantics can't?
Accepted answer
11 votes

There is no real agreement what characterises denotational semantics (see also this article), except that it must be compositional. That means that if $\newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \...

View answer
How to make a language homoiconic
Accepted answer
11 votes

You can make any language homoiconic. Essentially you do this by 'mirroring' the language (meaning for any language constructor you add a corresponding representation of that constructor as data, ...

View answer
Is model theory useful for computer scientists
11 votes

A special case of model theory is finite model theory which is closely related to complexity theory and database theory. However the methods being used in classical model theory (e.g. types, stability ...

View answer
What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?
Accepted answer
10 votes

I don't know why people didn't develop Hoare logics for lambda-calculi earlier. The first work to get this right was Honda et al's A Compositional Program Logic for Polymorphic Higher-Order Functions ...

View answer
Why is it important for functions to be anonymous in lambda calculus?
10 votes

I would like to venture an opinion that is different from those of @babou and @YuvalFilmus: It is vital for pure $\lambda$-calculus to have anonymous functions. The problem with having only named ...

View answer
Example of an algorithm that lacks a proof of correctness
10 votes

Most algorithms have not been proven correct in Hoare logic. The main reason is that such correctness proofs are extremely expensive as of Jan 2017, probably by several orders of magnitude in ...

View answer
Why does the state remain unchanged in the small-step operational semantics of a while loop?
10 votes

The state can change in subsequent reduction steps because on the right hand side of $$ \langle while\ B\ do\ S, \sigma \rangle \quad\rightarrow\quad \langle if\ B\ then\ ( {\color{red}{S}};\ ...

View answer
Framework or tools to generate theorem prover/solver/reasoner for new logic
Accepted answer
10 votes

There are many related ways you can mechanise your logic. Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using ...

View answer
Intro to Martin-Löf type theory
10 votes

I'm not aware of easy pathways into Martin-Löf type theory. I guess the following could serve as introductions. B. Nordström, K. Petersson, J. M. Smith, Martin-Löf's Type Theory. B. Nordström, ...

View answer
Bridge theorems for group theory and formal languages
10 votes

A famous area of study in the theory of group presentations is the word problem for groups. A group presentation is given by a bunch of generators $g_1, ..., g_m$ and a bunch of equations $a_1 = b_1, ....

View answer
Lambda Calculus in Rewriting systems
Accepted answer
9 votes

See also this question: "How is Lambda Calculus a specific type of Term Writing system?". Term rewriting, as introduced in (1), and described in e.g. (2), is a first-order system that cannot handle ...

View answer
Relation between Type Assignment system (TA) and Hindley-Milner system
Accepted answer
9 votes

System F and its subsystem HM have a type former for universal quantification: $$ \tau \quad::=\quad \forall x.\tau \ |\ ... $$ which the system in Hindley/Seldin doesn't have. That is the key ...

View answer
Why do some authors not include summation in the $\pi$-Calculus?
9 votes

To answer this question, it's best to reflect on the meaning of sums in process calculi. Essentially sums express a lack of knowledge. The process $P + Q$ means something along the lines of "either $P$...

View answer
Why isn't the Swift programming language type inference more aggressive?
9 votes

I don't understand Swift's typing system yet, so I can only speculate, but I imagine that it's for the same reason that Scala doesn't have full type inference: nobody knows how to do it in a ...

View answer
What does Tarski's Fixed-Point theorem give us that that Y-Combinator does't
Accepted answer
9 votes

If by Tarski's fix point theorem you mean the Knaster–Tarski fixpoint theorem, then it's widely applicable and very general. All you need is a complete lattice and a monotone function on the lattice. ...

View answer
Finite State Automata Within A Compiler
8 votes

You don't need to know FSAs for writing a compiler, provided you use a lexer generator that writes the lexer for you. In parts the emphasis on FSAs in compiler books is historical: fast lexing used ...

View answer
Is there a theory of exception hierarchies?
8 votes

There's a large number of publications on exceptions, with quite a few theoretical investigations. Here is an unstructured and far from complete list with some examples. Sorry, I don't have time at ...

View answer
How Types avoids Russel's Paradox?
Accepted answer
7 votes

There is a second solution to the conundrum, which is Quine's NF (New Foundations) set theory. NF is a set theory that avoid the paradox, but a set of all sets does exist. NF avoids Russell's paradox ...

View answer