mafribe · HackerTrans

8 tháng trướcdiscuss

Exactly.

Taiwan has spent the approx 120 years on a very different political, economic, cultural track from the mainland. Taiwan diverged from the other subject of the Qing dynasty before Han nationalists began their century long project to forge a united Chinese nation. In particular, Taiwan did not go through decades of communist terror, but did experience the fruit of democracy.

mafribe

9 tháng trướcdiscuss

Could you give some evidence for this claim? Here is some counterevidence: [1] says that the top buyers of Russian energy include:

• Hungary: 416 million euros ($488m)

• Slovakia: 275 million euros ($323m)

• France: 157 million euros ($184m)

• Netherlands: 65 million euros ($76m)

• Belgium: 64 million euros ($75m)

[2] suggests that China and India are the main buyers. I don't how reliable those sources are. There is also the problem of how to classify 'laundered' oil that was bought and resold by, e.g. India.

[1] https://www.aljazeera.com/news/2025/10/3/how-much-of-europes...

[2] https://energyandcleanair.org/june-2025-monthly-analysis-of-...

mafribe

2 năm trướcdiscuss

Neuromorphic has been an ongoing failure (for general purpose processors or even AI accelerators), ever since Carver Mead introduced (and quickly abandoned them) them nearly half a century ago. Bill Dally (NVidia CTO) concurs: "I keep getting those calls from those people who claim they are doing neuromorphic computing and they claim there is something magical about it because it's the way that the brain works ... but it's truly more like building an airplane by putting feathers on it and flapping with the wings!" From: Hardware for Deep Learning, HotChips 2023 keynote.

We have NO idea how the brain produces intelligence, and as long as that doesn't change, "neuromorphic" is merely a marketing term, like Neurotypical, Neurodivergent, Neurodiverse, Neuroethics, Neuroeconomics, Neuromarketing, Neurolaw, Neurosecurity, Neurotheology, Neuro-Linguistic Programming: the "neuro-" prefix is suggesting a deep scientific insight to fool the audience. There is no hope of us cracking the question of how the human brain produces high-level intelligence in the next decade or so.

Neuromorphic does work for some special purpose applications.

mafribe

3 năm trướcdiscuss

CNNs are from the 1980s (the "neocognitron" by Kunihiko Fukushima [1]), while the MLP is from 1958 [2]. So nearly half a century, resp. a century old.

[1] K. Fukushima, Neocognitron: A Self-organizing Neural Network Model for a Mechanism of Pattern Recognition Unaffected by Shift in Position.

[2] F. Rosenblatt, The Perceptron: A Probabilistic Model For Information Storage And Organization in the Brain.

mafribe

3 năm trướcdiscuss

Yes, Hinton was on a temporary position at the University of Sussex (IIRC, the Centre for Cognitive Science) for a while, but was not offered a permanent academic position there when he applied.

mafribe

10 năm trướcdiscuss

I'm not sure I can agree. Every language that is being heavily used eventually acquires meta-programming extensions of some sort of other.

mafribe

10 năm trướcdiscuss

   Artificial Intelligence is because 
   metaprogramming is easier in homoiconic 
   languages.

Homoiconicity is something you can add to any language, dynamically or statically typed, simple or complex, it doesn't matter. It used to be belived that only syntactically simple languages like Lisp are suitable for homoiconic extension, but this myth was destroyed by Walid Taha and his development of the MetaML family of languages.

For an overview of how to add homoiconicity to languages, see https://arxiv.org/abs/1602.06568

mafribe

10 năm trướcdiscuss

Yes, that's definitely one of the great things about Scala.

If you come from an OO background, I recommend to avoid using Scala's functional features at the start. Just treat Scala as a nice, conventional OO language until you are comfortable with the language. Then, slowly use some of the more advanced features. Case classes and pattern matching are easy and powerful next steps.

Enjoy the ride!

mafribe

10 năm trướcdiscuss

I'm afraid I disagree. I went from Ocaml to Scala. While full type inference is nice, it's a minor issue in practise, but the vastly bigger library ecosystem that Scala has (due to being a JVM language) isn't. Object orientation also works better in Scala than Ocaml.

mafribe

11 năm trướcdiscuss

Very nice descriptions.

While constructive reasoning is has many advantages, it has one disadvantage that is rarely pointed out, but sometimes causes real trouble.

Let's say we have a formula A which is classically and constructively true. It may be the case that constructive proofs of A are longer and more complicated than classical proofs of A. If you are working with an interactive proof assistant, this may be the difference between the proof automation being able to deal with A automatically or not.

This explosion in proof size is the reason why the (perfectly constructive) nominal techniques of Pitts et al have been implemented to a high standard in Isabelle/HOL are are used frequently, but are not really in Coq.

mafribe

11 năm trướcdiscuss

No.

Classically, LEM and double negation are equivalent.

Intuitionistically the situation is more complicated, see the discussion in this thread by IngoBlechschmid: We can prove that LEM implies double negation, but not the other way around. Intuitionistically, we can only prove that ⊢¬¬A⊃A, then ⊢A∨¬A, but not ⊢(¬¬A⊃A)⊃(A∨¬A).

For these and related reasons, double negation is not considered constructivistically valid.

mafribe

11 năm trướcdiscuss

I don't think synthetic homotopy type theory is known to cover all of conventional homotopy theory, so it's work in progress.

mafribe

11 năm trướcdiscuss

    A proof in mathematics is not purely syntactic because it's not purely logical.

This is confusing constructive reasoning with the decision problem for proof validity. They are different things.

The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make use of non-logical axioms of the ambient theory. If proof-hood is not decidable, it's not a logic.

Reasoning is constructive if it avoids certain proof principle like LEM (law of excluded middle) or double negation.

mafribe

11 năm trướcdiscuss

While Goedel's first incompleteness theorem indeed shows that there will always be true statements that don't follow from a given set of (computable) axioms, this is almost never a problem in practise. It is hard to find natural examples of such statements. Almost every mathematical statement (or its negation) you or I can come up with is a consequence of the axioms of ZFC set theory, or whatever other foundation you prefer.

mafribe

11 năm trướcdiscuss

Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathematics, they don't forget real numbers.

You need to distinguish between non-computable and non-constructive. The proof that the cardinality of the reals is non-countable is perfectly constructive, see [1] for a discussion of these and related issues.

[1] https://en.wikipedia.org/wiki/Cantor%27s_first_uncountabilit...

mafribe

11 năm trướcdiscuss

j2kun's characterisation of HoTT is misleading.

    Their goal is also to rewrite all of mathematics in a constructive way,

This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive.

HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/. You can say that HoTT derives non-constructive mathematics on top of constructive foundations.

   The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive)

No. Whether a proof can be logically checked by a computer has nothing to do with whether it is constructive or not. A proof is just a syntactic object. It's just as easy to check if a proof step uses excluded middle or double negation as it is to check whether it uses a construtive principle like /\-introduction. There are many proof assitants that work with classical logic, e.g. Mizar, HOL, HOL light, Isabelle/HOL ... All of SAT-solving works classically.

The novelty of HoTT, and only extension over intensional Martin-Loef type-theory, is the univalence axiom.

mafribe

11 năm trướcdiscuss

Typing systems (at least some of them) are also logics. This is called the Curry-Howard correspondence (CHC).

At first the CHC was made to work for propositional logic only, i.e. logic without for-all and existential quantification. Later typing systems were developed which correspond to logic with quantification. This requires dependent types. However, early typing systems with dependent types had an inelegant handling of equality. Logic needs equality to express things like forall x. x = 3 => x > 2. To overcome this problem, Per Martin-Loef introduced a dependent type-theory (MLTT) with "identity-types" which enables an elegant handling of equality. MLTT and all other extant formalisations of mathematics still suffered from another problem, in that many mathematical constructs are 'morally' the same, but formally distinct. For example you can define a group to be a triple ( G, 1, * ) where G is a set, 1 the neutral element and * the binary operation, or you can define it as ( G, *, 1 ). The former and the latter are not the same thing, but we don't really want to say that they formalise different concepts. This is similar to how in many programming languages certain types are formally distinct but somehow capture the same content.

Homotopy type theory (HoTT) overcomes this problem (or parts of this problem) by adding a single axiom to MLTT, called the "univalence axiom" which can informally be rendered as:

   Things that are 'morally' the same, really are identical.

The key idea behind the univalence axiom is that MLTT (and hence HoTT) restricts the mathematical objects that can be constructed such that whenever you have objects O1 and O2 that are morally the same, then there is a function that transforms any construction involving O1 automatically into a construction involving O2 or vice versa, but in a truth preserving way.

It turns out that proofs in HoTT are formally similar to certain aspects of geometry/topology.

Much of current research on HoTT is about the consequences of the univalence axiom and the similarity between logic and geometry/topology.

The key hope in all this is that HoTT will streamline formalised mathematics.

mafribe

11 năm trướcdiscuss

   reconciliation in my mind between dependent types and higher kinded types.

They are orthogonal concepts. This is made very clear in Barendregt's λ-cube [1]. Orthogonal here means that a typing system might be higher-kinded without allowing type-dependency, or it might allow type-dependency without having higher-kinds. An example of the latter is LF, the Logical Framework of Harper et al. Haskell, or at least some forms of Haskell are an example of the former.

Higher-kinded types simply allow functions and function application at the type level which can take functions as arguments and can return functions. For example (lambda x.x => bool) and (lambda xy. x => y) are functions at the type level.

An example of a dependent type is List(2+4)[bool], of lists of length 6 carrying booleans. Here (2+4) is a program. This parameterisation happens without having type-functions.

[1] https://en.wikipedia.org/wiki/Lambda_cube

comments