js8

20 ms·

361.
by js8 1y ago
I appreciate the answer.
362.
by js8 1y ago
I agree they can be answered, but easily - no. The Grobner basis algorithm has been known for longer than NP problems, so it's not obvious why it wasn't used to solve SAT problems.
363.
by js8 1y ago
One way to recover XORs from 3SAT (AFAIK unfortunately DIMACS doesn't support XOR natively) is to use the formula: (a | b | c) = ((a ^ ~x) | b) & (x | c) where x is a variable that can be chosen. The LHS is satisfiable iff RHS is s
364.
by js8 1y ago
I agree with the suggestion to study Haskell, I like Haskell quite a lot (although I don't write applications in it).
365.
by js8 1y ago
I don't understand why SAT solvers don't use gaussian elimination more. Every SAT problem can be represented as an intersection of linear (XORSAT) and 2SAT clauses, and the linear system can resolve some common contradictions, pro
366.
by js8 1y ago
"Words are allowed to have contextual meanings" Sure, but this discussion is about FCIS, that's the context, and the GP should consider that. " think I need a more precise meaning of "business logic" before I c
367.
by js8 1y ago
> I think they are orthogonal at worst, and in agreement at best. I have considered them being orthogonal, but then the definition of the "shell" and "core" becomes problematic in this comparison. What you call shell
368.
by js8 1y ago
I don't think your opinion about LLMs inner workings changes anything in what I said. Extremely open-minded people also don't care about facts in the sense they just accept whatever their perception of reality is, with no prejudic
369.
by js8 1y ago
"Generic core, specific shell." Your advice is the opposite of "functional core, imperative shell". The FCIS principle has IS which is generic, to be simple, because it's usually hard to test (it deals with resource
370.
by js8 1y ago
Actually, naive AGI such as LLM is way more intelligent than a human. Unfortunately, it does not make it smarter.. let me explain. When I see your comment, I think, your assumptions are contradictory. Why? Because I am familiar with Russell
371.
by js8 1y ago
I just had a similar discussion with a coworker, he was advocating that LLMs are practically useful, but I argued they are kinda bad because nobody knows how they really work. I think it's somewhat return to pre-enlightenment situation
372.
by js8 1y ago
No, latent space doesn't have to be made of percels, just like not every 2D array of 3-element vectors is an image made of pixels. Percels are tied to your sensors, components of what you perceive, in totality. Of course there is an in
373.
by js8 1y ago
How is this new compared to https://www.paecon.net/PAEReview/issue53/KeenStandish53.pdf ? (See the section "perfect competitors are not profit maximizers".)
374.
by js8 1y ago
Thanks for the pointer to MicroHS, looks interesting. BTW, this is probably obvious to you, there are also 5 combinators to which you can directly translate (with proper parentheses) the bits of BLC expression and it sort of self-evaluates
375.
by js8 1y ago
What is interesting though, the fastest interpreters for lambda calculus (such as yours uni.c) work by translating the term to combinatory logic (although with a bigger base than S,K) and calculating with it.
376.
by js8 1y ago
Yes, I just coined the neologism. It was supposed to be partly sarcastic (why stay at pixels, why not just go fully multimodal and treat the missing channels as missing information?), I am kind of surprised why it got so upvoted. (IME, ofte
377.
by js8 1y ago
Not pixels, but percels. Pixels are points in the image, while a "percel" is unit of perceptual information. It might be a pixel with an associated sound, in a given moment of time. In case of humans, percels include other senses
378.
by js8 1y ago
> Don't you mean xA = B ? No, that equation can be created as a special case from equation TAx = B (where Txy = yx is a transposition combinator). > Not if you require x to be strict, i.e. it must use its argument. I am not sure
379.
by js8 1y ago
Sometimes you can prove mathematically that two different approaches are equivalent, but differ only in name or some parameter, and that's a unification of sorts, without proliferation of standards. In case of UIs, this is still an ope
380.
by js8 1y ago
Yes, that's deliberate though. (I will call these "concrete" terms, because they lack abstraction in the body, but I am looking for a good name. In fact, no universal one-point basis can be expressed as a single term like tha
381.
by js8 1y ago
A CIL to LC compiler is effectively an emulator of CIL in LC. That is, every primitive of CIL has a corresponding LC term, which operates on the CIL execution state. So then you can express functions from .NET standard library as terms in L
382.
by js8 1y ago
Forth is an imperative language and as such you will have to model memory state (at least) somehow, if you want to use purely functional language as a representation. But that's the cost of doing business. The thing is though, you don&
383.
by js8 1y ago
> assuming everyone would use the same hardware, same environment and same workflows They don't have to. I would ideally represent HW, OS and compiler in the LC as well. Then primitives of the language that could be proven to be HW&
384.
by js8 1y ago
But why stop at Racket? Why not reduce the needed primitives even further down to LC?
385.
by js8 1y ago
Not really a big fan, because the formalization of DS always left something desired, but I think a big difference with formalization in ULC is that ULC is (mostly) materialist while DS is structuralist. So the initial formalization into ULC
386.
by js8 1y ago
I think this is great. I think you should write a paper on it. I suspect it might need some kind of commutative diagram proof, i.e. if you express things in CoC formalized within BLC you will get the same result as when you express in BLC f
387.
by js8 1y ago
I feel the same, too many people doing similar stuff in slightly different syntax, too few people looking at how things are similar and could be unified. I think it's time to look beyond syntax in programming and untyped lambda calculu
388.
by js8 1y ago
That's a rather cheap retort. I am not saying everybody should use raw untyped lambda calculus for their programming, just that we would all benefit if we could translate languages we use to and from it, because then we could interoper
389.
by js8 1y ago
Well, I feel that lot of code is written again and again, just in different languages. If we could automatically compare and translate different implementations, I think it would be beneficial for finding bugs. Everytime somebody comes up w
390.
by js8 1y ago
Not quite true, depends on the flavor of the type system you use. Church's simply typed is not, but other type systems are. I think one way to make it Turing complete is to add typing rule for Y combinator as an axiom to your simple ty

More ›