The PBE / IPS (= programming-by-example / inductive program synthesis)
literature cares about this a great deal. The approach to PBE / IPS in
the tradition of [1], essentially seeks a unique representative of
each equivalence class of programs w.r.t. to the usual typed notion of
program equivalence.
Since most interesting examples of PBE / IPS use recursion, [1] goes
through a hierarchy of recursion principles, e.g. map, filter, fold,
full recursion. The order of choosing recursion principles matters a
great deal for controlling overfitting, the bête noire of machine
learning.
The basic problem is this: the answer to the question "What terms have this type?" is almost always an infinite set with a great deal of redundancy. E.g. 2+3 and 3+2 are both an answer to "What terms have type Int?". But both answers are contextually indistinguishable, so in practise we only one to see one of them. Since contexual equivalence is typically undecidable there are limits to how clever you can be in a computer program to avoid redundancies. Moreover, in PBE / IPS you typically don't want to have just values, you are interested essentially in short programs inhabiting a type. So cut-eliminiation, at least as conventionally understood, doesn't quite do the job.
[1] J. K. Feser, S. Chaudhuri, I. Dillig, Synthesizing Data Structure
Transformations from Input-Output Examples.
Thanks! This looks like a really interesting part of PL theory that I haven't looked at before. The problem you describe immediately reminds me of Equality Saturation; I wonder if it's been applied in this space: http://www.cs.cornell.edu/~ross/publications/eqsat/
Well the common technical problem is that of representing program fragments along with their equalities so that they can be utilized in the case I linked, and pruned in the case you suggested. It's just a musing though. I look forward to reading up on PBE in depth.
Since most interesting examples of PBE / IPS use recursion, [1] goes through a hierarchy of recursion principles, e.g. map, filter, fold, full recursion. The order of choosing recursion principles matters a great deal for controlling overfitting, the bête noire of machine learning.
The basic problem is this: the answer to the question "What terms have this type?" is almost always an infinite set with a great deal of redundancy. E.g. 2+3 and 3+2 are both an answer to "What terms have type Int?". But both answers are contextually indistinguishable, so in practise we only one to see one of them. Since contexual equivalence is typically undecidable there are limits to how clever you can be in a computer program to avoid redundancies. Moreover, in PBE / IPS you typically don't want to have just values, you are interested essentially in short programs inhabiting a type. So cut-eliminiation, at least as conventionally understood, doesn't quite do the job.
[1] J. K. Feser, S. Chaudhuri, I. Dillig, Synthesizing Data Structure Transformations from Input-Output Examples.