HackerTrans
トップ新着トレンドコメント過去質問紹介求人

jfmc

no profile record

コメント

jfmc
·2 か月前·議論
!/0 is the cut. It prunes the search space. Useful to say "do not look at the other alternatives since I know they will fail" (when mutually exclusivity is hard) but also necessary to do negation in Prolog (when negated information cannot be easily or efficiently propagated).

is/2 is arithmetic evaluator. It runs only in one direction and it does not solve equations.

#>, #=, etc. are constraints, like (in)equalities over linear arithmetic. When constraints have the form of some known theory (like in SMT solvers), they can be solved (incrementally). That is called "constraint logic programming" (CLP). Modern Prolog systems are indeed CLP systems.

Prolog is older than CLP. CLP is older than SMT. Prolog+CLP systems are turing complete, can be used as programming languages. SMT is powerful but not a programming language.

Can "impure" features be avoided? Not in all cases. Think of them as 'unsafe' in Rust, but less dangerous.

Markus pushes for more purity in Prolog (using CLPFD), but sometimes some impurity (or imperative-like code with side-effects) is the best solution. Sometimes the pure solution is also the better. In other cases, it is not. Better compilers and static analyzers can reduce the friction between these worlds.

Take away: do pure code if you can afford it and it looks like a natural solution to your problem, use impure features later if you really need them.
jfmc
·8 か月前·議論
Right!
jfmc
·8 か月前·議論
Not a mathematician, but AFAIK ZFC is a valid foundation. Dependent types helps a lot with bookkeeping, but cannot prove more theorems.

Lawrence Paulson is a great person to clarify those topics (Isabelle/HOL is not based on types yet it can proof most maths).
jfmc
·8 か月前·議論
Not sure... Other Prologs compiled to WASM with very good performance is https://ciao-lang.org/playground/

The same toplevel runs also from 'node' as well.
jfmc
·昨年·議論
Other playground (wasm based): https://ciao-lang.org/playground
jfmc
·2 年前·議論
Actually, most of the paper seems a bit obvious from the computer science side. LLMs scale for really complex tasks, but they are neither correct nor complete. If combined with a tool that is correct (code verifiers, interactive theore provers), then we can get back a correct pipeline.
jfmc
·2 年前·議論
Wrong capitalization makes me feel really axious and frustrated.
jfmc
·2 年前·議論
Many times the algorithm that you are implementing requires a precise data flow that is not reversible, so using traditional arithmetic (is/2) is better for catching errors.

On the other hand CLP(FD) is not new at all (it is very popular for constraint programming).
jfmc
·2 年前·議論
A classic library, you can play with it here: https://ciao-lang.org/playground/#https://github.com/ciao-la...
jfmc
·2 年前·議論
No constraint optimization can replace Pentafunk Jenny ;)
jfmc
·2 年前·議論
Prior art: Eisenfunk - Pong (https://www.youtube.com/watch?v=cNAdtkSjSps)
jfmc
·2 年前·議論
Xapian is used in https://www.djcbsoftware.nl/code/mu/ for indexing emails.
jfmc
·2 年前·議論
Another table (in the same thread) comparing more systems: https://swi-prolog.discourse.group/t/porting-the-swi-prolog-...
jfmc
·2 年前·議論
Note that "CheerpX enables you to run existing 32-bit x86 native binaries". For some reason support for wasm64 (in browsers) has been stagnated for years, which is a pity.
jfmc
·3 年前·議論
WASM is an extremely useful compilation target because of its portability (specially for running on browsers), but it is far from being the "default compilation target" for almost any language. The promised near-native speed is not here (in general you get x2 or x3 slower code but it can be even worse), it is limited to 32-bits (MEMORY64 is on the way but there is not a clear roadmap of when this will be generally available in browsers), blocking IO is a pain, and its design seems to be constrained by the underlying JS JIT (it still looks like ASM.JS with a different syntax).

I still believe that it is a miracle that we have WASM as a standard, and that it runs smoothly across different browser vendors, but why nobody seems to be worried about lack of progress in performance?

LLVM IR would be a much better binary target. It was used in the abandoned PNaCL project. AFAIK Apple uses it (bitcode) to store apps that are later compiled for specific platforms. WASM looks like a toy compared with this technology.
jfmc
·5 年前·議論
A Facebook-controlled metaverse, rising gas prices... it is only a matter of time that humans ends up being used as batteries.