Analogical type theory

  • Bo Yi
  • Jiafu Xu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 722)


This paper proposes an analogical type system based on ITT. Based on the intuitive meaning of analogy, a set of rules are introduced and justified to deal with analogy. Analogies on types as well as terms are introduced in our system. By an analogy between types, we mean a pair of mappings satisfying coherent conditions on those types. Terms with analogous types are analogical if their focus points meet with each other under the analogy of the types. Analogical theorem proving and term derivation methods are also illustrated as examples of applications of our system.


Coherent Condition Natural Deduction Type Constructor Introduction Rule Intuitive Meaning 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Roland C. Backhouse, Paul Chisholm. Grant Malcolm and Erik Saaman, Doit-your-self type theory, Formal aspects of Computing, No 1, pp. 19–84, 1989.CrossRefGoogle Scholar
  2. 2.
    J. Carbonell, Derivational Analogy: A Theory of Reconstructive Problem Solving and Expertise Acquisition, in R. S. Michalski et al(ed.), Machine Intelligence: An Artificial Intelligence Approach, Morgan Kaufmann, 1986.Google Scholar
  3. 3.
    Dershowitz, N., Programming by Analogy, in: R. S. Michalski, J. G. Carbonell and T. M. Mitchell (Eds), Machine Learning II: An Artificial Intelligence Approach, Morgan Kaufmann, Los Altos, CA, 1986, pp. 395–423.Google Scholar
  4. 4.
    Dietzen, S. R. and W. L. Scherlis, Analogy in Program Development, in: The Role of Language in Problem Solving 2, J. C. Boudreaux, B. W. Hamill, and R. Jernigan(Eds), North-Holland, 1987, pp. 95–115.Google Scholar
  5. 5.
    W. A. Howard, The formulae-as-types notion of construction, in ‘To H. B. Curry: essay on conbinatory logic, λ-calculus and formalism', ed. Hindely J. R. and Selidin J. P., Academic Press, New York, 1980.Google Scholar
  6. 6.
    George Polya, Induction and Analogy, Princeton Hall, 1957Google Scholar
  7. 7.
    Masateru, Harao, Analogical Reasoning for Natural Deduction Theorem Proving, in (Edited by Zhongzhi Shi) Automated Reasoning, IWAR 92 (Beijing' China) pp. 220–228Google Scholar
  8. 8.
    Jianguo, Lu, Analogical Program Derivation Based on Type Theory, To appear in Theoretical Computer Science Vol.113.Google Scholar
  9. 9.
    Per Martin-Lof, Constructive Mathematics and Computer Programming, in Logic, Methodology and Philosophy of Science, pp. 153–175, North Holland, 1982.Google Scholar
  10. 10.
    Bengt Nordstrom, Kent Petersson and Jan M. Smith, Programming in Mation-lof's Type Theory, Clarendon Press (Oxford) 1990.Google Scholar
  11. 11.
    Takeuti, G. Proof Theory, North-Holland, (2nd. edition), 1987.Google Scholar
  12. 12.
    Bo, Yi and Jiafu, Xu, A Survey on Analogy Reasoning, Computer Science (in Chinese), 1989, No. 4, pp. 1–8Google Scholar
  13. 13.
    Bo, Yi, Analogy Model and Analogy Correspondence:A Formal Theory on Analogy, Doctorial Thesis of Nanjing University, December 1989.Google Scholar
  14. 14.
    Bo, Yi and Jiafu, Xu, Analogy Calculus, To appear in Theoretical Computer Science vol. 113, May 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Bo Yi
    • 1
  • Jiafu Xu
    • 1
  1. 1.Institute of Computer SoftwareNanjing UniversityNanjingP. R. China

Personalised recommendations