5 ms·

I know that this question is being asked and reseached -- indeed I do research in this direction. But it's not well understood, and it's not nearly as widely as

I know that this question is being asked and reseached -- indeed I do research in this direction. But it's not well understood, and it's not nearly as widely asked a question as the type-inference question which the java compiler asks every time you type something like int n = 2 + 3; Note that 2+3 needs to be type-inferred. cut elimination / normalization, I'm not sure this can be reduced to cut-elimination, because the question "What terms have this type?" can be asked for non-terminating programs as well -- indeed it becomes much more interesting. https://arxiv.org/abs/1607.04156 Aside: I'm not following HoTT closely, I guess the problem whether canonicity of the natural number type holds in HoTT in general (= can be derived from the axioms of HoTT alone) is still open?

danharaj 8y ago
> I'm not sure this can be reduced to cut-elimination, because the question "What terms have this type?" can be asked for non-terminating programs as well -- indeed it becomes much more interesting. Oh please share some references :) I think in that context what matters is the progress and preservation parts of cut elimination. > Aside: I'm not following HoTT closely, I guess the problem whether canonicity of the natural number type holds in HoTT in general (= can be derived from the axioms of HoTT alone) is still open? I haven't either, but I think that's the case.
- YorkshireSeason 8y ago
  share some references 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.
  - danharaj 8y ago
    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/ http://www.cs.cornell.edu/~ross/publications/eqsat/
    - YorkshireSeason 8y ago
      That's interesting, although from scanning the abstract, I don't immediately see the connection between ES and PBE.
      - danharaj 8y ago
        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.

danharaj 8y ago

> I'm not sure this can be reduced to cut-elimination, because the question "What terms have this type?" can be asked for non-terminating programs as well -- indeed it becomes much more interesting. Oh please share some references :) I think in that context what matters is the progress and preservation parts of cut elimination. > Aside: I'm not following HoTT closely, I guess the problem whether canonicity of the natural number type holds in HoTT in general (= can be derived from the axioms of HoTT alone) is still open? I haven't either, but I think that's the case.

YorkshireSeason 8y ago
share some references 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.
- danharaj 8y ago
  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/ http://www.cs.cornell.edu/~ross/publications/eqsat/
  - YorkshireSeason 8y ago
    That's interesting, although from scanning the abstract, I don't immediately see the connection between ES and PBE.
    - danharaj 8y ago
      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.