espeed

Here is a link to the corresponding SIGMA 2018 paper and a link to the video shown at the end of the talk, which shows an animation illustrating the conjectures in the paper.

An animation illustrating the conjectures [video] https://www.youtube.com/watch?v=Ru0Zys1Vvq4

The Intro begins...

  These conjectures resulted from our attempts to
  understand data obtained following a 9 month
  calculation in magma on a supercomputer at the MPIM
  in Bonn. These results go far beyond existing 
  calculations and are obtained using a new algorithm.
  The algorithm relies in an essential way on ideas of 
  Libedinsky, Riche and the second author. The behaviour 
  we observe appears highly non-trivial, which suggests 
  that proving anything might be difficult.

Billiards and Tilting Characters for SL3 [pdf]

http://emis.ams.org/journals/SIGMA/2018/015/sigma18-015.pdf

Here's the code: https://github.com/nykh/cs242-lambda-pi

Carl Jung termed the phenomenon synchronicity [1], "which holds that events are 'meaningful coincidences' if they occur with no causal relationship yet seem to be meaningfully related." Google the philosophy of information, phenomenology, and "the world is made of meaning." Also related is the phenomenon of multiple discovery / simultaneous invention [2]. Ironically, this is in-part what the Curry–Howard correspondence is about, with the Church–Turing thesis being a prime example [3].

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

[2] https://en.wikipedia.org/wiki/Multiple_discovery

[3] https://en.wikipedia.org/wiki/Church–Turing_thesis

My burgeoning conjecture (as hinted at in a previous comment) is that all can be unified, transformed, and optimized for modern hardware under the matrix model of computation -- type theory, the lambda calculus, the actor model, neural nets, graph computing -- I'm starting to see a path to where all models are aligned across vectors of unity.

Here are some the correspondences I've been looking at...

* Graph algos in the lang of linear algebra now realized and encoded into GraphBLAS [1]

* The three normed division algebras are unified under a complex Hilbert space [2]

* Ascent sequences and the bijections discovered between four classes of combinatorial objects [3]

* Dependent Types and Homotopy Type Theory [4]

* Bruhat–Tits buildings, symmetry, and spatial decomposition [5]

* Distributed lattices, topological encodings, and succinct representations [6]

* Zonotopes and Matroids and Minkowski Sums [7]

* Holographic associative memory and entanglement renormalization [8]

[1] Graph Algorithms in the Language of Linear Algebra (Jeremy Kepner) http://www.mit.edu/~kepner/ Discussion: https://news.ycombinator.com/item?id=18099520

[2] Division Algebras and Quantum Theory (John Baez) http://math.ucr.edu/home/baez/rch.pdf

[3] (2 + 2)-free posets, ascent sequences and pattern avoiding permutations [pdf] https://www.sciencedirect.com/science/article/pii/S009731650...

[4] Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities [pdf] https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf

[5] Bruhat–Tits buildings and p-adic Lie groups https://en.wikipedia.org/wiki/Building_(mathematics)

[6] Distributive lattices and Stone-space dualities https://en.wikipedia.org/wiki/Distributive_lattice#Represent...

[7] Solving Low-Dimensional Optimization Problems via Zonotope Vertex Enumeration [video] https://www.youtube.com/watch?v=NH_CpMYe3tw https://en.wikipedia.org/wiki/Zonohedron

[8] Entanglement Renormalization (G Vidal) https://authors.library.caltech.edu/9242/1/VIDprl07.pdf?hovn... Holography https://en.wikipedia.org/wiki/Holographic_associative_memory

Google Scholar: https://scholar.google.com/scholar?q=related:Yi-GtarGxh0J:sc...

Philip Wadler provides an in depth discussion on the Curry–Howard correspondence [0] in his paper Propositions as Types [1], and he has given several talks under the same name that are on YouTube.

The talk Prof Wadler gave at Strange Loop is the most cited, but the talk he gave at Stanford [2] is the most interesting because Carl Hewitt was in the audience and was challenging him on the merits and long-term viability of functional programming in general vs Hewitt's Actor Model [3] for scalable concurrent computing.

[0] Curry–Howard correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence

[1] Propositions as Types [pdf] http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-...

[2] Propositions as Types (Stanford) [video] https://www.youtube.com/watch?v=ivzpaiw26wQ Slides [pdf] http://www.inf.ed.ac.uk/teaching/courses/tspl/pat.pdf

[3] Actor Model https://en.wikipedia.org/wiki/Category:Actor_model_(computer...

The significance of this paper is not about learning the λ-calculus.

Rather, to me the significance of this paper is that it presents a novel way of "implementing the lambda calculus in an algebraic system" and provides a correspondence between the λ-calculus and the matrix model of computation:

  Vector and matrix valued functions can be represented
  by vectors and matrices some of whose entries are 
  lambda expressions.

I have been looking for a lingua franca for programming languages, a way to unify the langs and make use of the decades of wisdom encoded into our langs' Great Libs. Maybe the matrix model and linear algebra is the lingua franca I seek.

NB: Better to refrain from saying stuff like "it completely misses the point" unless you are certain you understand the point beyond the level presented.

NB: the file command tries to identify file types via file sigs (magic numbers) stored in /usr/share/file/magic, for more mysterious file types or partials, you'll need to use one of the other methods.

NB: I suspect the number you are thinking of is a 2530 digit sequence on a 4-digit lock, not 153 on 5...

https://en.wikipedia.org/wiki/De_Bruijn_sequence#Uses

Yes, and in this case the sequence is specifically the "classic" De Bruijn sequence [1]; however, there are other sequences that bear De Bruin's name, such as the Moser de Bruijn sequence, which is the one I reference most due to its relation to Z-order curves and pairing functions.

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

[2] https://en.wikipedia.org/wiki/Moser-de_Bruijn_sequence

Type-driven development, meta languages, specs, provably correct code, and automatic code generation were some of the big overlapping themes at Strange Loop [1] this year. All the talks posted online this week [2], and I've posted links to some of the related videos below [3].

It's a good indicator that the time has come for an idea when multiple lines of research and projects from disparate domains begin converging on the same idea from different directions.

Several facets of the puzzle I've been working the last few years have converged towards this area so it's good to see that it's not just me, maybe that means we're all on the right track. But as 'pron and those who have been working in this area have pointed out [4], this part of the puzzle is not yet solved, and one of the primary open issues is how to scale it to the system level (beyond provably correct programs to provably correct systems).

One of the questions I've been pondering is how can we combine provably correct software specs with hardware specs identified for any given system to find the optimal data structures and algorithms given the constraints of that architecture.

Does something similar already exist? What's the best software currently out there for simulating ideal data flow for a given hardware configuration and a given set of system constraints?

[1] Strange Loop https://www.thestrangeloop.com

[2] Strange Loop 2018 talks (80 videos) https://www.youtube.com/playlist?list=PLcGKfGEEONaBUdko326yL...

[3] Related videos...

* Vellvm - Verifying the LLVM, by Steve Zdancewic https://www.youtube.com/watch?v=q6gSC3OxB_8

* All the Languages Together, by Amal Ahmed https://www.youtube.com/watch?v=3yVc5t-g-VU

* Towards Language Support for Distributed Systems, by Heather Miller https://www.youtube.com/watch?v=IeBbiQZYmuY

* Data Driven UIs, Incrementally, by Yaron Minsky https://www.youtube.com/watch?v=R3xX37RGJKE

* Proof Theory Impressionism: Blurring the Curry-Howard Line, by Dan Pittman https://www.youtube.com/watch?v=jrVPB-Ad5Gc

* A Little Taste of Dependent Types, by David Christiansen https://www.youtube.com/watch?v=VxINoKFm-S4

* You are a Program Synthesizer, by James Koppel https://www.youtube.com/watch?v=ldkF-4WNZqA

[4] open issue is how to scale it to the system level https://news.ycombinator.com/item?id=18253680

> Good specifications are often written at a level that generating executable code from them is often undecidable and almost always intractable in practice.

What about modern dependently-typed meta languages like Idris and program synthesizers like Nadia Polikarpova's work on Synquid?

Type-Driven Program Synthesis, by Nadia Polikarpova (StrangeLoop 2018) [video] https://www.youtube.com/watch?v=HnOix9TFy1A

MIT Comcom: Synquid program synthesizer, and more command-line tools for the web

http://comcom.csail.mit.edu/comcom/

Idris Software Foundations https://github.com/idris-hackers/software-foundations

No hits??? Or no callbacks after first contact?

Send me your resume, and I'll take a look (email in profile).

Who are the founders?

What is their background?

What are they selling?

Who are they selling to?

No. That ship has sailed. The new runtime is in the browser. Learn about wasm and matrix-multiply-add.

No, don't think like that. Concurrency is becoming more important, that's just the new reality on the other side of Moore's Law. Concurrency doesn't just happen. Someone has to design the AWS Lambda concurrency model and build the system to scale even if it's not you. And unless the system's design is improving over time and approaching optimal, eventually no one's going to use it because it will cost more than it should so people will move on toward the optimal one. And just like we have multi-layer caching models, distributed means we now have multi-layer concurrency models. Message passing Actors might be optimal between nodes, but within nodes matrix-multiply tensor models running on GPU/TPU accelerators is where optimal's at. And unless you understand it, you won't even be on the map.

And that capabilities model is one of the big differences in Pony and was the key to achieving Pony's parallel lock-free provably correct concurrency model.

Most lang/system capability models (including Go's) are open from the start -- where anyone can do anything -- and then when designing the lang/system you try to restrict access between some things at some of the time, but this gets messy fast and it's hard to get right and thus it's almost never optimal.

So rather than trying to start with an open model that's inherently flawed by definition, Pony flips the model on its head and begins from the perspective that everything is denied unless specified. You would say Pony has a deny-first capabilities model, which you can see explicitly defined here in Pony's capabilities matrix...

https://soyyomakesgames.wordpress.com/2016/10/10/ponys-capab...

And if you listen to Sylvan's talks, he is emphatic that solving the capabilities problem upfront was key that made everything else possible. All the other cool stuff you hear about in Pony like the provably correct runtime and finally achieving something approaching Hewitt's elusive Actor model that's been theoretically true for 40 years but never fully realized. Well the key to solving that mystery and unlocking the door was to take a new view on the capabilities model and building everything off that from the start.

Pony's new novel lock-free Actor model is of considerable note. Sylvan (https://github.com/sylvanc) has since joined MSR Cambridge and is working on the distributed model now...

https://github.com/ponylang/ponyc

https://www.ponylang.io/discover/#what-is-pony

https://www.youtube.com/results?search_query=ponylang

You're referring to the distributed Actor model?

What lang ecosystem with an interactive REPL do you see as the best fit for pairing with and driving Pony?

I've been dreaming of ways to help bootstrap the Pony lang/lib interop story and build toward a numerical interactive programming environment, being able to combine Pony's native async Actor model and runtime safety guarantees, while also safely being able to hook into to an external ecosystems existing numerical computing, data structure, and GPU/TPU accelerator libs.

I seem to remember someone giving a lang talk a while back where in the Q&A the speaker said integrating with Pony might be a good fit. I was looking into dependent types at the time...it may have been Idris or OCaml, and hooking into the Julia ecosystem would be most interesting, with maybe even Zig acting like low-level LLVM glue code binding all the external C libs together.

In my dream I have it all and the Pony too! All the lang libs are hooked together in a typed-provable way, and when fully connected they combine to form a high-performance, interactive parallel distributed programming environment, and it runs in the browser too. What do you think, is that too much of a DeepDream?

One of the common traits is an inability to access higher-order cognitive functions such as empathy and being unaware of their inability to do so. This often means they're in a chronic state of anxiety and confusion because the intentions of others make no sense. Conflating empathy for low affect feelings of sympathy while assuming an identity of the most empathetic and most sympathetic person in the world, maybe even thinking they're HSP. Here's one way you can find out and discover to what extent that's factoring into the mix.

Next time you find yourself in a situation where they are behaving contrary to what you would expect, don't assume malice. Make sure you carefully and clearly articulate your feelings and perspective, have them voice their concerns, and then ask them to rearticulate what you just said. Ask them to put into their own words what you are thinking and feeling, to rearticulate what your perspective is and why. Ask them to explain the cause and effect of their actions. And then shut up and let them answer, see what happens. Pay close attention to how they respond, to what extent they can empathise even if it's just simply repeating back what you said. You both may be shocked -- them by the question, you by the response -- but it'll be an enlightening experience. And after a time or two of that, at least you'll know where you are.

Yeah, succinct data structures aren't something taught in most intro to data structures courses, and the concept may even be unfamiliar to oldhats since SDSs are relatively new on the scene -- the public datasphere only started becoming conscious of the idea in 1988 when Guy Jacobson introduced them in his CMU thesis. And I have yet to find a digital copy of it online so for those who want to read the original thesis, you may have to order a paper copy of one or go to the CMU library to read it.

https://scholar.google.com/scholar?q=guy+jacobson

But, there's been a lot of development on succinct data structures since, and this post on the fast select algorithm was in-part a continuation of a conversation from a post yesterday on succinct data structures in general and the open-source lib SDSL 2.0. So if anyone wants to learn more about SDSs in general, there's a bunch of links to videos and reference material in the comments of yesterday's thread...

SDSL – Succinct Data Structure Library 2.0 https://news.ycombinator.com/item?id=18204432

Yep, often misdiagnosed as BPD or one of the Cluster B's, come to find out Asperger's is on the same spectrum. One of the most confounding situations I've ever experienced.

https://en.wikipedia.org/wiki/Cluster_B_personality_disorder...

Well, if it's true, we finally have a real live answer to the age-old question in Iron Eagle: "Dad, will the Maverick fire if we're still on the ground?" [1]

https://en.wikipedia.org/wiki/Iron_Eagle

[1] https://www.imdb.com/title/tt0091278/quotes

McLuhan's Understanding Media is a seminal work and one of the books that most shaped my thinking. "Electric Speed is synonymous with light and with the understanding of causes..." That line inspired the name for the Internet consulting company I formed in 1999, and espeed has been my online handle ever since.

  At no period in human culture have men understood 
  the psychic mechanisms involved in invention and 
  technology. Today it is the instant speed of electric 
  information that, for the first time, permits easy 
  recognition of the patterns and the formal contours of 
  change and development. The entire world, past and 
  present, now reveals itself to us like a growing plant 
  in an enormously accelerated movie. Electric speed is 
  synonymous with light and with the understanding of
  causes.

  — Marshall McLuhan, Understanding Media: The Extensions of Man (1964)

> Everything is a device!

There Are No Things. [0] ... only actions and properties. Everything is an actor [1].

In his Turing lecture, Robin Milner wrote [2]:

  Now, the pure lambda-calculus is built with just two 
  kinds of thing: terms and variables. Can we achieve 
  the same economy for a process calculus? Carl Hewitt, 
  with his Actors model, responded to this challenge 
  long ago; he declared that a value, an operator on 
  values, and a process should all be the same kind of 
  thing: an Actor.

  This goal impressed me, because it implies the 
  homogeneity and completeness of expression ... But it 
  was long before I could see how to attain the goal in 
  terms of an algebraic calculus...

  So, in the spirit of Hewitt, our first step is to 
  demand that all things denoted by terms or accessed by 
  names--values, registers, operators, processes, 
  objects--are all of the same kind of thing; they 
  should all be processes.

And now today Hewitt's elusive true mythical Actor model may have finally been realized and embodied in a language called Pony [3].

[0] https://www.edge.org/response-detail/11514

[1] https://en.wikipedia.org/wiki/Actor_model#Fundamental_concep...

[2] https://en.wikipedia.org/wiki/Actor_model#Theory

[3] https://github.com/ponylang/ponyc

To be precise, this is about the bitlevel SDS rank and select operation.

https://en.wikipedia.org/wiki/Succinct_data_structure

Hi Todd - Has your team looked at GraphBLAS [1] yet for MapD [2] now that Tim Davis has released a 2.0 reference C implementation (included in SuiteSparse 5.3) [3]? There is a GraphBLAS 2.0 CPU implementation in RedisGraph now [4] and official GraphBLAS 2.x GPU implementations are in the works.

[1] GraphBLAS http://graphblas.org

[2] OmniSci MapD DB https://github.com/omnisci/mapd-core

[3] SuiteSparse::GraphBLAS http://faculty.cse.tamu.edu/davis/suitesparse.html

[4] Previous Discussion https://news.ycombinator.com/item?id=18099520

Previous discussion in 2015 with the main authors: https://news.ycombinator.com/item?id=10157558

See Bradley's comment wrt to licensing the fractal tree code as GPLv2 w/ a patent provision https://news.ycombinator.com/item?id=18208209