In lambda calculus, this is called beta-equivalence, and is undecidable. (Renaming of variables is called alpha-equivalence, and is typically assumed implicitly.) If you know that two expressions both have beta normal forms, then by the Church-Rosser theorem, you can decide their equivalence by computing their normal forms and comparing for identity.
In some systems of typed lambda calculus, every expression has a normal form, so equivalence is decidable for the whole language, but the cost of that is that the language will not be able to express all computable functions. In particular, you may have difficulty shoehorning a program that can talk about itself into such a system. Self-reference is a basilisk for systems of logic, ever since Russell knocked down Frege’s system by saying, “what about the set of sets that are not members of themselves?”
There are results along these lines for term rewriting systems and graph rewriting systems also.
Decidability of equivalence is broken somewhere between simply typed lambda calculus and System-F. Without recursive types you are strongly normalizing and thus “trivially” decidable. However, just adding recursive types does not break decidability (e.g. see http://www.di.unito.it/~felice/pdf/ictcs.pdf). Similarly, just adding some higher-order functions or parametric polymorphism does also not necessarily break decidability (e.g. see Hindley-Milner). In my (admittedly limited) experience, when making a type system stronger, it is usually some strange, sometimes subtle interaction of these “type system features” that break decidability.
So the first problem raised in the OP is probably tractable for many, quite expressive type systems, even including recursive types.
Though I fully agree with you that the second problem is usually how undecidability proofs start and I’m more skeptical towards that one.
In lambda calculus, this is called beta-equivalence, and is undecidable. (Renaming of variables is called alpha-equivalence, and is typically assumed implicitly.) If you know that two expressions both have beta normal forms, then by the Church-Rosser theorem, you can decide their equivalence by computing their normal forms and comparing for identity.
In some systems of typed lambda calculus, every expression has a normal form, so equivalence is decidable for the whole language, but the cost of that is that the language will not be able to express all computable functions. In particular, you may have difficulty shoehorning a program that can talk about itself into such a system. Self-reference is a basilisk for systems of logic, ever since Russell knocked down Frege’s system by saying, “what about the set of sets that are not members of themselves?”
There are results along these lines for term rewriting systems and graph rewriting systems also.
Decidability of equivalence is broken somewhere between simply typed lambda calculus and System-F. Without recursive types you are strongly normalizing and thus “trivially” decidable. However, just adding recursive types does not break decidability (e.g. see http://www.di.unito.it/~felice/pdf/ictcs.pdf). Similarly, just adding some higher-order functions or parametric polymorphism does also not necessarily break decidability (e.g. see Hindley-Milner). In my (admittedly limited) experience, when making a type system stronger, it is usually some strange, sometimes subtle interaction of these “type system features” that break decidability.
So the first problem raised in the OP is probably tractable for many, quite expressive type systems, even including recursive types.
Though I fully agree with you that the second problem is usually how undecidability proofs start and I’m more skeptical towards that one.