semi-unification

• To: types@theory.LCS.MIT.EDU
• Subject: semi-unification
• From: Gert Smolka <SMOLKA%DS0LILOG.BITNET@mitvma.mit.edu>
• Date: Mon, 17 Jul 89 17:50:19 EDT
• Sender: meyer@theory.LCS.MIT.EDU

Date:         Mon, 17 Jul 89 20:08:47 CET

I've become interested in semi-unification (see the LICS 89 paper
of Kfouri et al., for instance).  Before I waste more time on it,
I would like to ask a few things:

1. Is the general problem still open (Kapur et al. solved it for
   one inequation, Kfouri et al. for inequations with linear LHSs)?

2. Is it clear why Kapur et al's techniques don't extend to the general
   case, or may they?

3. Are there people expecting the problem to be undecidable?
   (It seems we have a proof that the problem is undecidable
    for rational trees ("cyclic terms"), but this proof really
    exploits the availibility of infinite trees).

Gert Smolka, IBM Deutschland, smolka@ds0lilog.bitnet

• Prev: Post doc position for work on SML compiler
• Next: Bounded Linear Logic
• Index(es):
  • Main
  • Thread