triska

50 ms·

421.
by triska 7y ago
Very nice list, thank you for the writeup and for sharing this! One interesting thing about the Emacs modes listed here is that many one of them are by themselves already enough to justify the use of Emacs for at least someone in specific a
422.
by triska 7y ago
Thank you for sharing this writeup! Regarding the Emacs example: You can make Emacs crash entirely by triggering internal recursion in the garbage collector that exceeds the C stack limit, for example with: $ emacs -Q --eval "(le
423.
by triska 7y ago
Thank you for the links! As stated in Tom Leinster's paper that you link to, both ZFC and Lawvere set theory are first-order theories: "In logical terminology, both axiomatizations [i.e., ZFC and Lawvere set theory] are simpl
424.
by triska 7y ago
Very nice! For comparison, here is a Prolog program that uses CLP(ℤ), constraint logic programming over integers, to search for solutions: solution(Options, Vs) :- A^5 + B^5 + C^5 + D^5 #= E^5, Vs = [A,B,C,D,E]
425.
by triska 8y ago
I used interpretation as it occurs for example in Computability and Logic by Boolos, Burgess and Jeffrey. It is also explained here: https://en.wikipedia.org/wiki/Interpretation_(logic)#Interpr... Please note that
426.
by triska 8y ago
The terminology of first-order logic is indeed quite different from that of Prolog. A key reason for this is that in FOL, we have to distinguish between the syntactic entities and their interpretations. So, in FOL, we have predicate symbol
427.
by triska 8y ago
Mercury's roots are indeed the explanation and justification for many of these points: Mercury syntax is deliberately designed to be very close to Prolog syntax. In fact, it is so close to Prolog that if you remove the declarations, th
428.
by triska 8y ago
Thank you so much for Emacs, and congratulations on the new release! Emacs is reliable, fast and elegant, and a joy to use as a truly integrated environment for all kinds of tasks, including software development.
429.
by triska 8y ago
Very nice, thank you for sharing this! Symbolic execution is also known as abstract interpretation . The program is being interpreted, with concrete values abstracted away , generalized to symbolic elements that often denote several or ev
430.
by triska 8y ago
Nice list! I noticed that the list also contains several corrigenda. However, there are corrigenda that are also publicly available yet not on this list. For example, the hitherto published corrigenda for the Prolog ISO standard (ISO/I
431.
by triska 8y ago
Logic programming is one such example. Prolog and its syntactic subset Datalog are taught as part of countless CS degrees throughout the entire world. In fact, logic in general is such an example. At least a basic treatment of proposition
432.
by triska 8y ago
Without context, one could indeed get this impression. However, Kurt Gödel and John von Neumann had met each other and exchanged letters long before that already, and Gödel was fully aware that von Neumann was interested in this area. For e
433.
by triska 8y ago
This would work if clause/2 always failed if there is no matching clause. Indeed, in some systems, that was the case. But now, clause/2 may and will throw an error for example on: ?- clause(true, B). ERROR: No permissi
434.
by triska 8y ago
Yes, a complete Prolog meta-interpreter would definitely be meta-circular. However, it is quite hard to write an interpreter for complete Prolog, both in Prolog and also in other languages. Take for example handling of !/0. It is not e
435.
by triska 8y ago
That's a very interesting topic and nice write-up, thank you for sharing! For comparison, here is a small interpreter for a subset of Prolog, written in Prolog: mi([]). mi([G|Gs]) :- clause_(G, Body),
436.
by triska 8y ago
This is awesome work, and also a truly great writeup! I particularly enjoyed the outline of iterations to improve performance. Thank you very much for putting this together! Emacs in general has great potential as a truly general programmab
437.
by triska 8y ago
Yes, you are right: This is not what Craig's theorem says! It is enough to assume that the theorems are recursively enumerable. From this, it follows that there is an axiomatization where the axioms are recursive. The key point is th
438.
by triska 8y ago
"Let our formal system be effectively axiomatized. Then by definition its axioms are a recursive set." "effectively axiomatized" means that the theorems are recursively enumerable. It does not immediately follow that
439.
by triska 8y ago
Thank you for adding this! Still, it is not so straight-forward to conclude, from just the premise that the system is effectively axiomatized (i.e., its theorems are recursively enumerable), that "does s prove S" is a recursive pr
440.
by triska 8y ago
In my opinion, this is true for some main points, but definitely not for all of them. A key difference between the languages is in how easily you can reason about programs. In Prolog, if you program in the pure monotonic subset of the l
441.
by triska 8y ago
In the paper, it is assumed — per footnote 1 — that the formal systems under discussion are effectively axiomatized. I assume this means that their theorems are recursively enumerable , is this correct? If so, then this means that determin
442.
by triska 8y ago
The proofs you present are entirely constructive and work without appealing to the law of the excluded middle! As was also pointed out by Gödel himself about his proofs, they are obtained in an "intuitionistically unobjectionable manne
443.
by triska 8y ago
That's a very nice writeup, thank you a lot! One thing that seemed a bit surprising to me, especially in light of the paper's strong focus on computation, is that the assumption that the axiomatization is effective is only menti
444.
by triska 8y ago
Thank you for sharing! One thing I noticed is the statement in 20. Logic: An axiom system is neither complete nor provably consistent. I think this would benefit from some rephrasing, because such a system could for example be both comple
445.
Programming Languages used for Machine Learning(vitalflux.com)
2 points by triska 8y ago|0 comments
446.
by triska 8y ago
That's a justified question! I'm using DCG (semicontext) notation here analogously to monads , mostly to benefit from having to keep track of fewer explicit arguments that need to be passed around. In this concrete case, using th
447.
by triska 8y ago
Thank you for sharing! For comparison, here is an interpreter for non-deterministic Turing machines, written in the logic programming language Prolog: turing(Name, Tape0, Rs) :- phrase(turing_(s(q0), Name), [[]-Tape0], [_-
448.
by triska 8y ago
In addition to the recommended CapsLock ⇒ LCtrl rebinding done on the OS level, there are also several things you can do within Emacs to edit and navigate comfortably. For example, you can add this to your ~/.emacs: (global-set-k
449.
by triska 8y ago
That's a very nice challenge! Here is a Prolog formulation of the task: :- use_module(library(clpfd)). n_tour(N, Vs) :- L #= N*N, length(Vs0, L), successors(Vs0, N, 1), append(
450.
by triska 8y ago
PostScript is an amazing programming language for describing scalable graphics and interfaces! I especially enjoy the ability to very concisely represent information, using dedicated PostScript facilities to construct domain-specific lang

More ›