I’m trying to decide if it would be quicker to (port to Smalltalk) or write new code?
If MMJ code is elegant/well designed, I will spend time reading it.
If MMJ is badly designed/messy code then I guess it will be quicker just to write new code without looking at MMJ?
What do you think?
> I’m trying to decide if it would be quicker to (port to Smalltalk) or write new code?
> If MMJ code is elegant/well designed, I will spend time reading it.
> If MMJ is badly designed/messy code then I guess it will be quicker just to write new code without looking at MMJ?
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CO3PR18MB4960DE0C165129DE46DE8975A46E9%40CO3PR18MB4960.namprd18.prod.outlook.com.
If U is the most general unifier of a set of expressions
then any other unifier, V,
can be expressed as V = UW,
where W is another substitution.
What’s the best thing to read to grok this algorithm?
MMJ? But I don’t know Java, so is there an algorithm in English?
thx
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CO3PR18MB49608C696D935ACE3E8DBE59A4719%40CO3PR18MB4960.namprd18.prod.outlook.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSshZ3X-s8%2Be%3D%3D0CpV-6NB2Az66Q_iQx3tsM0iX-_0Pupg%40mail.gmail.com.
Are there any more implementations anyone wants to offer, please?
I think it's quite possible that anything goes when it comes to writing a unification algorithm? Maybe it doesn't matter in the slightest how you come by a unification, because the very next thing you're going to do is run a validator to ensure the proof is correct anyway, and because a perfect algorithm does not currently exist so you're always going to have to be able to fall back on the option of manual unification. Heuristics, AI, quantum superposition of all potential unifications, whatever. I'll almost certainly stick to the standard algorithm anyway, but it might become tempting to massage away some difficulties (if any) encountered while attempting to re-unifying theorems in set.mm.
Are there any more implementations anyone wants to offer, please?I think it's quite possible that anything goes when it comes to writing a unification algorithm? Maybe it doesn't matter in the slightest how you come by a unification, because the very next thing you're going to do is run a validator to ensure the proof is correct anyway, and because a perfect algorithm does not currently exist so you're always going to have to be able to fall back on the option of manual unification. Heuristics, AI, quantum superposition of all potential unifications, whatever. I'll almost certainly stick to the standard algorithm anyway, but it might become tempting to massage away some difficulties (if any) encountered while attempting to re-unifying theorems in set.mm.Or maybe it does matter because it's important to know whether it's the proof or the unification that was wrong.Best regards,Antony
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9471eb0d-3807-4446-a191-a99b5a92b2c8n%40googlegroups.com.