p0llard · HackerTrans

p0llard

no profile record

Submissions

Ask HN: Why don't you use formal methods?

8 pointsby p0llard6 ปีที่แล้ว4 comments

Ask HN: What added value do academic publishers provide?

8 pointsby p0llard6 ปีที่แล้ว11 comments

MIT Emergency Management: Students reimbursed $500 to leave campus by Sunday

emergency.mit.net

2 pointsby p0llard6 ปีที่แล้ว0 comments

Ask HN: How do you organise PDFs/eBooks?

12 pointsby p0llard6 ปีที่แล้ว4 comments

Formal Reasoning About Programs (2017) [pdf]

adam.chlipala.net

83 pointsby p0llard7 ปีที่แล้ว23 comments

Formal Reasoning About Programs (2017) [pdf]

adam.chlipala.net

3 pointsby p0llard7 ปีที่แล้ว0 comments

comments

6 ปีที่แล้วdiscuss

> Gödel's statements are true in all models

This is wrong, and I said the exact opposite of this: there are non-standard models of PA in which G_F is false.

There is a fundamental difference between Gödel sentences and AoC, which is that the Gödel sentence is Pi_1, which means its independence implies its truth in the standard model.

I'm just not really a fan of unqualified "true" meaning "true in the standard model"; I think if you're doing a course purely on the incompleteness theorems for an audience without much exposure to mathematical logic, using "true to refer to "truth in the standard model" is not a good idea and is likely to lead to misconceptions.

Perhaps the fact that you think G_F is true in all models is evidence in favour of my claim?

6 ปีที่แล้วdiscuss

> Question: Can a sentence be provably true in one arithmetic system but not another?

The answer is yes!

    ZFC |- AC

but

    ZF |/- AC

and both ZFC and ZF can encode arithmetic.

But there's an issue here: no-one really talks about the "truth" of the Axiom of Choice as though it's a concrete thing: it's a very controversial axiom, and although most mathematicians accept it, quite a few don't. Constructivist mathematicians don't accept it, and it's provably equivalent to the law of the excluded middle, so it can't be used in intuitionistic logics.

Now you might counter and say that AC isn't the Gödel sentence for ZFC, and the Gödel sentence for PA is true in the intended model. But that's a different matter from whether it's provable from an axiomatic foundation. The reason I think this matters is because mathematicians work with proofs! Most mathematicians aren't working in foundations, and rely on proofs to the extent that they don't even consider the truth of statements which cannot be proven.

> If so that means there are provably true sentences which exist, but not provably true with the axioms that I have at my disposal right now?

The issue is that provability is completely contingent on the set of axioms you use: provability isn't a universal notion. Of course if you add something which is unprovable (such as the Gödel sentence) to PA, you get a new system which can prove more things: but this system has its own unprovable Gödel sentence.

I'd also question what you mean by "provably true": a sentence is provable from a theory when there exists a derivation in some proof calculus of the sentence starting from the axioms of the theory. "True" is much harder to pin down, and we wouldn't usually say "provably true". "True" can mean "true in the intended model", "true in all models", or even just "provable from a set of axioms".

The Gödel sentence is "true but unprovable" only in the sense that it is true in the intended model: it is not a tautology.

I think most people who have had a brief exposure to mathematics would consider "true in all models" (i.e. tautological truth) to be what is meant by "true", so I don't like it being used to mean "true in the intended model" without qualification.

6 ปีที่แล้วdiscuss

> I feel like you may be arguing semantics

Yeah, I am; it really depends on how you define "true". I prefer this to be interpreted as "true in all models" so sentences are "true" when they are tautological consequences of a theory.

Using this definition, all "true" sentences are provable in first-order logic.

The (usual) Gödel sentence is true in the intended model of arithmetic, but I don't really like this property being referred to as "truth" without qualification.

> "true but unprovable" within a given system

Not sure about this: I don't think you can really say something is "true in a system" if it isn't provable. You can only assert its truth by saying it's "true in the intended model" without qualification, or by doing some meta-reasoning in a more powerful system outside the original one.

6 ปีที่แล้วdiscuss

> There are true statements that are unprovable within the system.

I really don't like this, and it verges on being flat-out incorrect: the first incompleteness theorem does not say this at all. It says that there are sentences (and indeed it constructs one, the so-called Gödel Sentence) that cannot be proven or refuted within the system.

For first-order theories it follows from the contraposition of Gödel's completeness theorem that there exist (classical) models of the theory where this sentence holds and models where it doesn't: the existence of models where the sentence does not hold means that this must be a very different meaning of "true" to the one used in common parlance.

In higher-order logics, which do not have a completeness theorem, it makes sense to talk about true statements which are unprovable: there can exist tautologies, sentences which hold in all models of a theory, which cannot be proven from the axioms of a higher-order theory (and you don't need the incompleteness theorem for this); on the other hand, in a first-order theory all tautologies are provable.

Sentences which cannot be proven or refuted within a theory are said to be logically independent of the theory. Famously, the Axiom of Choice is independent of the axioms of Zermelo–Fraenkel set theory: it's up to mathematicians to decide whether they accept the Axiom of Choice. If they do, they can work in ZF+C; if not, they can work in ZF. Neither system is "more true" from a purely logical perspective, so I really don't like describing logically independent sentences as "true but unprovable": it almost certainly doesn't mean what people think it means.

The first incompleteness theorem could perhaps be stated better for a lay audience as:

    No recursive set of axioms can capture our notion of arithmetic it its entirety.

This is a limitation on how we can use axiom systems to represent mathematical objects: even more informally, we might say:

    Truth is subjective in sufficiently complex systems.

6 ปีที่แล้วdiscuss

> Godel-type unprovability is separate from logical independence

What do you mean by this? The Goedel sentence of a system is logically independent from the system by the standard meaning of "logical independence".

6 ปีที่แล้วdiscuss

> true but unprovable under the axioms xyz?

Careful: we don't really talk about things which are "true but unprovable" in first-order logics.

By Goedel's completeness theorem, if a statement is true in all models of a first-order theory then it is provable. For any recursively axiomisable first-order theory of sufficient complexity, there exists some sentence which isn't provable [Goedel's First Incompleteness Theorem]: by contraposition of completeness, there exist models of the theory where the sentence is true, and models where the sentence is false.

So when you say "true but unprovable", you're probably talking about truth in the so-called "intended model": if something is independent of the first-order system (e.g. ZF) you're using as a foundation of mathematics, then you get to decide whether it's true or not! Once you've proven independence via e.g. forcing, it's up to you to decide whether the sentence should hold in your intended model: then you can add the appropriate axiom to your system.

Choice is independent from ZF: most mathematicians are OK with choice, so they chose to work in ZFC, but some aren't. Neither is "more valid" or "more true" from a purely logical perspective.

6 ปีที่แล้วdiscuss

> And, you realize that the US has 300m people, correct? You will have to compare per-capita stats, not total numbers.

The UK has a population of almost 70MM. The factor of ~5 needed to account for population pales in comparison to the two orders of magnitude difference between 25 days and 25 years.

6 ปีที่แล้วdiscuss

> According to a judge or a police officer, probably not

I'd naively hope that a judge wouldn't side with a police officer here, but I think the fact that resisting arrest is inherently criminal is a pretty big flaw in the US legal system.

I live in a jurisdiction [1] where resisting arrest is not criminalised in the same sense as the US, and the idea that a police officer could unlawfully arrest you and then immediately have lawful grounds if you resisted is very alien to me.

[1] : https://en.wikipedia.org/wiki/Resisting_arrest#England_and_W...

6 ปีที่แล้วdiscuss

I live in a country where we don't inject people with ketamine on the street, nor do "criminals run amok". We also don't have armed gangs imposing "their own idea of a justice system", and we have fewer police killings in 25 years than the US has in 25 days.

I imagine your comment is probably symptomatic of the major societal issues within the US; it certainly worsens the image of the US to those fortunate enough to live in a Western nation which isn't actively regressing.

6 ปีที่แล้วdiscuss

> Want to work with an IP vendor whose sales are not part time lawyers? Go for ARM

Interested in this comment: were MIPS/Imagination known for being particularly litigious around licensing?

6 ปีที่แล้วdiscuss

> Why would you guess?

Because I'm basing it on my experience doing research in PLT, but this is of course purely anecdotal and my areas of research interest lie away from the likes of Haskell, so I would not wish to make a false claim by stating it as fact.

> Why is this [more] important?

I never said that it was, only that depending on what is meant by "leading", industry usage might not be relevant. Since Scala is by far the more used language I think it's fair to assume that (without meaning to put words into mouths) the original commenter might have been talking about PLT research as opposed to usage in industry.

6 ปีที่แล้วdiscuss

Yes it is, but if "leading functional language" means "on the cutting edge of research into functional languages" then that might well be used to describe Haskell.

If leading refers to overall usage in industry, then sure, it's not really relevant.

6 ปีที่แล้วdiscuss

Yeah I think you're definitely right, and Algorithm W is how HM was introduced to me when I studied it.

kevincox's comment sums up my misunderstanding.

6 ปีที่แล้วdiscuss

In general they seem to do a good job of missing out books which cover the mathematical basis of theoretical computer science; if the aim is to provide a starting point for humanity to recover technical knowledge following some disaster, I'd argue that a survey of the past 100 years' research into theoretical computer science is orders of magnitude more useful (who wants to repeat (i.e. waste) another 100 years on the Entscheidungsproblem?) than n different books on specific programming language.

6 ปีที่แล้วdiscuss

Probably depends on the definition of leading; I'd guess that Haskell is probably used more than any other (Turing-complete, to exclude Gallina, etc.) functional language within programming language research, but you're right that in terms of usage in industry etc. Scala is probably on top.

6 ปีที่แล้วdiscuss

> There exist many type inference algorithms, the best known one is the so-called Algorithm W.

Is this correct? I dug out Milner's paper [1] where he states that Algorithm J is more efficient (which was what I had been led to believe), but that Algorithm W is more suited to functional (as opposed to imperative) implementations.

Edit: Actually I think I'm parsing this sentence incorrectly, "best known" means literally that as opposed to "most efficient known".

[1] https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/...

6 ปีที่แล้วdiscuss

When I said "incompatible at the physical level" I meant it in the OSI sense of an issue at physical protocol level. An electrical specification mismatch could easily cause hardware damage (but would be very hard to achieve unless you were using your own PHY or literally connecting a power supply to the PCIe lines).

> seems pretty minimal

Is there actually any at all? I can't really see how this could lead to any damage.

6 ปีที่แล้วdiscuss

> tinker with advanced stuff requiring PCI-E chipsets

What sort of things are you talking about here, out of interest? The only way you're going to wreck hardware is if you're attaching something completely incompatible at the physical level (wrong levels, shorts, etc.); if you're "tinkering" you almost certainly don't have the resources to bring up your own PCIe PHY (there's pretty much no way to do this without custom silicon) so presumably you have some preexisting hardware in mind?

If you just want to play around at the TLP level (for example by using the hard PCIe core in a cheap Xilinx Series-7 chip) then this is all pretty safe: (temporary) catastrophic system instability is one thing (I learned this the hard way when I accidentally had my FPGA spamming MSIs every free cycle), but real hardware damage is pretty tricky.

6 ปีที่แล้วdiscuss

> He's working on the same ledger tech but centralised

Cryptographic ledger technology has been around since forever (the 70s to be precise): just look at Git, SUNDR, etc.

I believe he's specifically calling out firms working on cryptocurrencies; cryptocurrencies are just one application of cryptographic distributed ledgers.

6 ปีที่แล้วdiscuss

They aren't really targeting similar markets (at least from my perspective): pretty much any multinational firm can benefit from better corporate treasury management; cryptocurrencies are just one application of this technology, and Stephen is calling out specifically those which are attempting to defraud (or at least benefit from the the gross ignorance of) retail investors.

Those seem like entirely different markets to me.