3 ms·
Qi II
- gruseom 18y agoHas anyone used this to build a serious system? I wonder if it is an undiscovered gem.
- palish 18y agoCan you give an example of an undiscovered gem?
- gruseom 18y agoNo idea why someone would downmod that but I have neutralized them. :) "Undiscovered" is of course a relative term. I'd cite the languages of Arthur Whitney here: they're "discovered" enough to have made a lot of money, but are unknown to the vast majority of the computing world and widely misunderstood even by those who have heard of them. Qi isn't absolutely "undiscovered" - here we are talking about it - but it's largely unknown and unused. Tarver strikes me as a smart guy doing serious work in an intelligent way. For example, building Qi on top of CL (in such a way that you can drop in to CL whenever you want, though this point is redundant) seems like an obvious win. I don't feel a need to use something that right now, but I'm also skeptical of the "I don't feel a need to use that" feeling... perhaps we are all Blub to Qi!
- jhancock 18y agoI've just spent the last hour of my Sunday afternoon reading through http://www.lambdassociates.org/MinimalManual http://www.lambdassociates.org/MinimalManual So far I'm impressed.
- malkia 18y agoDirectory Listing Denied This Virtual Directory does not allow contents to be listed.
- rw 18y agoDemanding money for the language manual/guide is not an inefficient way to increase adoption!
- utx00 18y ago<sarcastic> sounds like fun </sarcastic> Unlike Qi I, Qi II allows you to embed sequent rules within functions, evaluating them to closures. These rule closures are type checked and are permeable to having their variables lexically bound from outside the scope of the rule itself. These devices enable the student of computational logic to effortlessly code complex logical systems of all descriptions. Thus the rule let PTerm/X (replace-by X Term P) PTerm/X, (all X P) >> Q; ____________________ (all X P) >> Q; allows universally quantified assumptions to be instantiated to new premises. This rule can be embedded into a Qi II function called all-left which does precisely this job. The rule is turned into a closure by the rule function which is then applied to the problem (list of sequents). (define all-left {term --> [sequent] --> [sequent]} Term S -> ((rule let PTerm/X (replace-by X Term P) PTerm/X, (all X P) >> Q; ____________________ (all X P) >> Q;) S))