fmap

16 ms·

211.
by fmap 10y ago
This is a nice proof. I just want to mention that it is also completely constructive - all objects involved are finite and so exhaustive search supplies the necessary instance of excluded middle. We really don't have a good terminology
212.
by fmap 10y ago
Any function f of type f : forall a b. (a -> b) -> F a -> F b Such that f id = id is automatically a functor (respects composition). In type theory, every equivalence is automatically natural. There's a lot more and it&
213.
by fmap 10y ago
In mathematics, I would describe category theory as an offshoot of structuralism. The main idea is that instead of starting with some "premodel" of what you want to study ("I want to study geometry on surfaces, so I'm lo
214.
by fmap 10y ago
Very cool project with a great name! If you haven't looked at it already, you may be interested in Arthur Charguéraud's work on program verification using characteristic formulas ( http://www.chargueraud.org/softs&
215.
by fmap 10y ago
If you demand that the program terminates (through higher order structural recursion, i. e. by induction) then this would be a proof in type theory. It's called proof by reflection. When Martin Löf (the father of type theory) saw this
216.
by fmap 10y ago
I can't speak for applications in physics, but in combinatorics and analytic number theory there is no magic involved. The idea in combinatorics is that you start by looking at the ring of infinite sequences over C with componentwise a
217.
by fmap 10y ago
It isn't so simple, unfortunately. The idea behind set theory was to describe some universal building blocks of mathematics. The problem is that - unlike in the case of computable functions - such a universal building block can't
218.
by fmap 10y ago
I think it's a nice analogy. It's a bit tongue in cheek, but it does give you the right idea when you compare it to programming languages. Set theory is a reductionistic system. It's supposed to give a foundation which is as
219.
by fmap 10y ago
In particular, there has been a ton of work on automating inductive proofs. So while I enjoyed the article, I'm not sure what's up with the first sentence. This is definitely not the first inductive theorem prover. Funnily enough,
220.
by fmap 10y ago
It comes down to levels of assurance. The rules of inference you are using are part of your design space. Mathematics at its core is about clever problem solving. When you encounter a problem you have to decide what you would accept as a
221.
by fmap 10y ago
If there are ever more compelling use cases for smart contracts this will create a market for smart contract validation or development. Interactive theorem proving is already at the level that verifying something like the DAO (a few hundred
222.
by fmap 10y ago
They make their money off of advertising. Facebook is competing with them in this regard and if they can't replace them, the next best thing would be to undercut the competition. I think that's the scenario the parent was thinking
223.
by fmap 10y ago
That is an actual engineering job. A colleague of mine used to work as a research programmer at cmu. This is what he was doing.
224.
by fmap 10y ago
Let's talk again in a few years. :) In all seriousness, though, I'm also just speaking from personal experience. That said, if you are working in type theory, chances are that you will end up skimming almost everything on this lis
225.
by fmap 10y ago
It's more of a vocabulary issue. In PL theory "type inference" is a well-defined concept. It means that you have the ability to reconstruct the types of a program without annotations. No mainstream (imperative) programming la
226.
by fmap 10y ago
You're seriously underestimating the amount of work that goes into a phd, or into writing a textbook...
227.
by fmap 11y ago
There is a lot of room for improvement with the implementation. The way we are using deep neural networks at the moment is exellent for prototyping, but far from optimal. For instance, this paper http://arxiv.org/abs/15
228.
by fmap 11y ago
Computer science is a broad field and not all of us are doing our PhDs in software engineering. There are some things which you just can't do in the industry yet, since the technology is not at a point where it is commercially viable.
229.
by fmap 11y ago
This is a wonderful series of articles and I find myself nodding along with most of it. However, these lines really made me cringe: A child was sent to me for tutoring because of failing a geometry class, and gave this excuse: " I
230.
by fmap 11y ago
Neat! Do you have some pointers to your work? I would be especially interested in example verifications of lock free data structures and in comparing the proof effort to logics custom built for this purpose. All the constructions I know use
231.
by fmap 11y ago
I am honestly unconvinced on "most of mathematics" being just ZFC. You see this claim a lot, but when reading formal developments in mathematics I often see justifications involving "small categories" or statements which
232.
by fmap 11y ago
There are several good reasons to call it Coq: - The person who implemented the first version (?) is called Coquand. - The french have a tradition of naming their software projects after animals. - Coq is french for Rooster. But to be hones
233.
by fmap 11y ago
Ok, there are a number of points you can make comparing set theory and type theory... but the most important point here is that it is a false dichotomy! From a logical point of view "type theory" is a particular formalism for desc
234.
by fmap 11y ago
KCC is certainly an achievement, but it doesn't subsume Robert's work. If you look into the linked thesis you'll find that a lot of the work deals with finding high-level descriptions of the C semantics. A major part of CH2O
235.
by fmap 11y ago
There are many classically equivalent formulations of the axiom of choice, the one I gave is just the one I like best. :) But you are right, the devil is in the details, so let me spell it out precisely: The axiom states that for every set
236.
by fmap 11y ago
The point is that there is one ordering in which every subset of real numbers has a minimum. For the rational numbers, this is not difficult, since we can enumerate the rational numbers. As the ordering we could then pick "a <= b&qu
237.
by fmap 13y ago
If I remember correctly there was even a special clause in the C standard definition of union types which allows you to write: struct A { Data header; ... } struct B { Data header; ... } union AB { Data header; A a; B b } and then access th
238.
by fmap 13y ago
There'd be 10+ different platforms which would be competing and innovating? Did I miss the implied sarcasm tag? If you look at OS research from the 80s it seems pretty clear that the industry never caught up.
239.
by fmap 13y ago
Yes. You can translate the classical proof, assuming excluded middle for propositions.
240.
by fmap 13y ago
Answer to auggierose's comment above: Yes you can prove that sqrt(2) is irrational. This is actually a great example, because it doesn't need excluded middle. Equality of rational numbers is decidable, which means that classical r

More ›