Eta-Reduction in Type-Theory of Acyclic Recursion
Abstract We investigate the applicability of the classic eta-conversion in the type-theory of acyclic algorithms. While denotationally valid, classic eta-conversion is not algorithmically valid in the type theory of algorithms, with the exception of few limited cases. The paper shows how the restricted, algorithmic eta-rule can recover algorithmic eta-conversion in the reduction calculi of type-theory of algorithms.
- Referencias
- Cómo citar
- Del mismo autor
- Métricas
Duží, M., 2019. If structured propositions are logical procedures then how are procedures individuated? Synthese, 196(4):1249–1283.
Duží, M. and Kosterec, M., 2017. A Valid Rule of β-conversion for the Logic of Partial Functions. Organon F, 24(1):10–36.
Duží, M. and Jespersen, B., 2012. Procedural isomorphism, analytic information and β-conversion by value. Logic Journal of the IGPL, 21(2):291–308. ISSN 1367-0751. doi:10.1093/jigpal/jzs044.
Gallin, D., 1975. Intensional and Higher-Order Modal Logic: With Applications to Montague Semantics. North-Holland Publishing Company, Amsterdam and Oxford, and American Elsevier Publishing Company. ISBN 0 7204 0360 X.
Loukanova, R., 2001. Russellian and Strawsonian Definite Descriptions in Situation Semantics. In Gelbukh, A., editor, Computational Linguistics and Intelligent Text Processing. CICLing 2001, volume 2004 of Lecture Notes in Computer Science, pages 69–79. Springer, Berlin, Heidelberg. ISBN 978-3-540-44686-6.
Loukanova, R., 2002a. Generalized Quantification in Situation Semantics. In Gelbukh, A., editor, Computational Linguistics and Intelligent Text Processing, volume 2276 of Lecture Notes in Computer Science, pages 46–57. Springer, Berlin, Heidelberg. ISBN 978-3-540-45715-2.
Loukanova, R., 2002b. Quantification and Intensionality in Situation Semantics. In Gelbukh, A., editor, Computational Linguistics and Intelligent Text Processing. CICLing 2002, volume 2276 of Lecture Notes in Computer Science, pages 32–45. Springer, Berlin, Heidelberg. ISBN 978-3-540-45715-2.
Loukanova, R., 2009. β-Reduction and Antecedent-Anaphora Relations in the Language of Acyclic Recursion. In Cabestany, J., Sandoval, F., Prieto, A., and Rodríguez, J. M. C., editors, Bio-Inspired Systems: Computational and Ambient Intelligence. IWANN 2009, volume 5517 of Lecture Notes in Computer Science, pages 496–503. Springer, Berlin, Heidelberg, Salamanca, Spain. doi:10.1007/978-3-642-02478-8.
Loukanova, R., 2011a. Modeling Context Information for Computational Semantics with the Language of Acyclic Recursion. In Pérez, J. B., Corchado, J. M., Moreno, M., Julián, V., Mathieu, P., Canada-Bago, J., Ortega, A., and Fernández-Caballero, A., editors, Highlights in Practical Applications of Agents and Multiagent Systems, volume 89 of Advances in Intelligent and Soft Computing, pages 265–274. Springer Berlin Heidelberg.
Loukanova, R., 2011b. Reference, Co-reference and Antecedent-anaphora in the Type Theory of Acyclic Recursion. In Bel-Enguix, G. and Jiménez-López, M. D., editors, Bio-Inspired Models for Natural and Formal Languages, pages 81–102. Cambridge Scholars Publishing.
Loukanova, R., 2019a. Computational Syntax-Semantics Interface with Type-Theory of Acyclic Recursion for Underspecified Semantics. In Osswald, R., Retoré, C., and Sutton, P., editors, IWCS 2019 Workshop on Computing Semantics with Types, Frames and Related Structures. Proceedings of the Workshop, pages 37–48. The Association for Computational Linguistics (ACL), Gothenburg, Sweden.
Loukanova, R., 2019b. Formalisation of Situated Dependent-Type Theory with Underspecified Assessments. In Bucciarelli, E., Chen, S.-H., and Corchado, J. M., editors, Decision Economics. Designs, Models, and Techniques for Boundedly Rational Decisions. DCAI 2018, volume 805 of Advances in Intelligent Systems and Computing, pages 49–56. Springer International Publishing, Cham. ISBN 978-3-319-99698-1.
Loukanova, R., 2019c. Gamma-Reduction in Type Theory of Acyclic Recursion. Fundamenta Informaticae, 170(4):367–411. ISSN 0169-2968 (P) 1875-8681 (E).
Loukanova, R., 2019d. Gamma-Star Canonical Forms in the Type-Theory of Acyclic Algorithms. In van den Herik, J. and Rocha, A. P., editors, Agents and Artificial Intelligence, pages 383–407. Springer International Publishing, Cham.
Loukanova, R., 2020. Algorithmic Eta-Reduction in Type-Theory of Acyclic Recursion. In Rocha, A., Steels, L., and van den Herik, J., editors, Proceedings of the 12th International Conference on Agents and Artificial Intelligence (ICAART 2020), volume 2, pages 1003–1010. INSTICC, CITEPRESS – Science and Technology Publications, Lda. ISBN 978-989-758-395-7.
Loukanova, R., 2023. Algorithmic Dependent-Type Theory of Situated Information and Context Assessments. In Omatu, S., Mehmood, R., Sitek, P., Cicerone, S., and Rodríguez, S., editors, Distributed Computing and Artificial Intelligence, 19th International Conference, volume 583, pages 31–41. Springer International Publishing, Cham. ISBN 978-3-031-20859-1. doi:10.1007/978-3-031-20859-1_4.
Moschovakis, Y. N., 1989. The formal language of recursion. Journal of Symbolic Logic, 54(4):1216–1252.
Moschovakis, Y. N., 1993. Sense and denotation as algorithm and value. In Oikkonen, J. and Väänänen, J., editors, Logic Colloquium ’90: ASL Summer Meeting in Helsinki, volume Volume 2 of Lecture Notes in Logic, pages 210–249. Springer-Verlag, Berlin.
Moschovakis, Y. N., 1997. The logic of functional recursion. In Dalla Chiara, M. L., Doets, K., Mundici, D., and van Benthem, J., editors, Logic and Scientific Methods, volume 259, pages 179–207. Springer, Dordrecht.
Moschovakis, Y. N., 2006. A Logical Calculus of Meaning and Synonymy. Linguistics and Philosophy, 29(1):27–89. ISSN 1573-0549.
Plotkin, G., 1975. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125–159. ISSN 0304-3975. doi:10.1016/0304-3975(75)90017-1.
Plotkin, G. D., 1977. LCF considered as a programming language. Theoretical Computer Science, 5(3):223–255.
Thomason, R. H., editor, 1974. Formal Philosophy: Selected Papers of Richard Montague. Yale University Press, New Haven, Connecticut.
Tichý, P., 1988. The foundations of Frege’s logic. In The Foundations of Frege’s Logic. Berlin: De Gruyter.
Tichý, P., 1995. Constructions as the Subject Matter of Mathematics. In Depauli-Schimanovich, W., Köhler, E., and Stadler, F., editors, The Foundational Debate: Complexity and Constructivity in Mathematics and Physics, pages 175–185. Springer Netherlands, Dordrecht. ISBN 978-94-017-3327-4. doi:10.1007/978-94-017-3327-4_13.
Duží, M. and Kosterec, M., 2017. A Valid Rule of β-conversion for the Logic of Partial Functions. Organon F, 24(1):10–36.
Duží, M. and Jespersen, B., 2012. Procedural isomorphism, analytic information and β-conversion by value. Logic Journal of the IGPL, 21(2):291–308. ISSN 1367-0751. doi:10.1093/jigpal/jzs044.
Gallin, D., 1975. Intensional and Higher-Order Modal Logic: With Applications to Montague Semantics. North-Holland Publishing Company, Amsterdam and Oxford, and American Elsevier Publishing Company. ISBN 0 7204 0360 X.
Loukanova, R., 2001. Russellian and Strawsonian Definite Descriptions in Situation Semantics. In Gelbukh, A., editor, Computational Linguistics and Intelligent Text Processing. CICLing 2001, volume 2004 of Lecture Notes in Computer Science, pages 69–79. Springer, Berlin, Heidelberg. ISBN 978-3-540-44686-6.
Loukanova, R., 2002a. Generalized Quantification in Situation Semantics. In Gelbukh, A., editor, Computational Linguistics and Intelligent Text Processing, volume 2276 of Lecture Notes in Computer Science, pages 46–57. Springer, Berlin, Heidelberg. ISBN 978-3-540-45715-2.
Loukanova, R., 2002b. Quantification and Intensionality in Situation Semantics. In Gelbukh, A., editor, Computational Linguistics and Intelligent Text Processing. CICLing 2002, volume 2276 of Lecture Notes in Computer Science, pages 32–45. Springer, Berlin, Heidelberg. ISBN 978-3-540-45715-2.
Loukanova, R., 2009. β-Reduction and Antecedent-Anaphora Relations in the Language of Acyclic Recursion. In Cabestany, J., Sandoval, F., Prieto, A., and Rodríguez, J. M. C., editors, Bio-Inspired Systems: Computational and Ambient Intelligence. IWANN 2009, volume 5517 of Lecture Notes in Computer Science, pages 496–503. Springer, Berlin, Heidelberg, Salamanca, Spain. doi:10.1007/978-3-642-02478-8.
Loukanova, R., 2011a. Modeling Context Information for Computational Semantics with the Language of Acyclic Recursion. In Pérez, J. B., Corchado, J. M., Moreno, M., Julián, V., Mathieu, P., Canada-Bago, J., Ortega, A., and Fernández-Caballero, A., editors, Highlights in Practical Applications of Agents and Multiagent Systems, volume 89 of Advances in Intelligent and Soft Computing, pages 265–274. Springer Berlin Heidelberg.
Loukanova, R., 2011b. Reference, Co-reference and Antecedent-anaphora in the Type Theory of Acyclic Recursion. In Bel-Enguix, G. and Jiménez-López, M. D., editors, Bio-Inspired Models for Natural and Formal Languages, pages 81–102. Cambridge Scholars Publishing.
Loukanova, R., 2019a. Computational Syntax-Semantics Interface with Type-Theory of Acyclic Recursion for Underspecified Semantics. In Osswald, R., Retoré, C., and Sutton, P., editors, IWCS 2019 Workshop on Computing Semantics with Types, Frames and Related Structures. Proceedings of the Workshop, pages 37–48. The Association for Computational Linguistics (ACL), Gothenburg, Sweden.
Loukanova, R., 2019b. Formalisation of Situated Dependent-Type Theory with Underspecified Assessments. In Bucciarelli, E., Chen, S.-H., and Corchado, J. M., editors, Decision Economics. Designs, Models, and Techniques for Boundedly Rational Decisions. DCAI 2018, volume 805 of Advances in Intelligent Systems and Computing, pages 49–56. Springer International Publishing, Cham. ISBN 978-3-319-99698-1.
Loukanova, R., 2019c. Gamma-Reduction in Type Theory of Acyclic Recursion. Fundamenta Informaticae, 170(4):367–411. ISSN 0169-2968 (P) 1875-8681 (E).
Loukanova, R., 2019d. Gamma-Star Canonical Forms in the Type-Theory of Acyclic Algorithms. In van den Herik, J. and Rocha, A. P., editors, Agents and Artificial Intelligence, pages 383–407. Springer International Publishing, Cham.
Loukanova, R., 2020. Algorithmic Eta-Reduction in Type-Theory of Acyclic Recursion. In Rocha, A., Steels, L., and van den Herik, J., editors, Proceedings of the 12th International Conference on Agents and Artificial Intelligence (ICAART 2020), volume 2, pages 1003–1010. INSTICC, CITEPRESS – Science and Technology Publications, Lda. ISBN 978-989-758-395-7.
Loukanova, R., 2023. Algorithmic Dependent-Type Theory of Situated Information and Context Assessments. In Omatu, S., Mehmood, R., Sitek, P., Cicerone, S., and Rodríguez, S., editors, Distributed Computing and Artificial Intelligence, 19th International Conference, volume 583, pages 31–41. Springer International Publishing, Cham. ISBN 978-3-031-20859-1. doi:10.1007/978-3-031-20859-1_4.
Moschovakis, Y. N., 1989. The formal language of recursion. Journal of Symbolic Logic, 54(4):1216–1252.
Moschovakis, Y. N., 1993. Sense and denotation as algorithm and value. In Oikkonen, J. and Väänänen, J., editors, Logic Colloquium ’90: ASL Summer Meeting in Helsinki, volume Volume 2 of Lecture Notes in Logic, pages 210–249. Springer-Verlag, Berlin.
Moschovakis, Y. N., 1997. The logic of functional recursion. In Dalla Chiara, M. L., Doets, K., Mundici, D., and van Benthem, J., editors, Logic and Scientific Methods, volume 259, pages 179–207. Springer, Dordrecht.
Moschovakis, Y. N., 2006. A Logical Calculus of Meaning and Synonymy. Linguistics and Philosophy, 29(1):27–89. ISSN 1573-0549.
Plotkin, G., 1975. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125–159. ISSN 0304-3975. doi:10.1016/0304-3975(75)90017-1.
Plotkin, G. D., 1977. LCF considered as a programming language. Theoretical Computer Science, 5(3):223–255.
Thomason, R. H., editor, 1974. Formal Philosophy: Selected Papers of Richard Montague. Yale University Press, New Haven, Connecticut.
Tichý, P., 1988. The foundations of Frege’s logic. In The Foundations of Frege’s Logic. Berlin: De Gruyter.
Tichý, P., 1995. Constructions as the Subject Matter of Mathematics. In Depauli-Schimanovich, W., Köhler, E., and Stadler, F., editors, The Foundational Debate: Complexity and Constructivity in Mathematics and Physics, pages 175–185. Springer Netherlands, Dordrecht. ISBN 978-94-017-3327-4. doi:10.1007/978-94-017-3327-4_13.
Loukanova, R. (2023). Eta-Reduction in Type-Theory of Acyclic Recursion. ADCAIJ: Advances in Distributed Computing and Artificial Intelligence Journal, 12(1), e29199. https://doi.org/10.14201/adcaij.29199
Most read articles by the same author(s)
- Roussanka Loukanova, Restricted Computations and Parameters in Type-Theory of Acyclic Recursion , ADCAIJ: Advances in Distributed Computing and Artificial Intelligence Journal: Vol. 12 (2023)
- Roussanka Loukanova, Relationships between Specified and Underspecified Quantification by the Theory of Acyclic Recursion , ADCAIJ: Advances in Distributed Computing and Artificial Intelligence Journal: Vol. 5 No. 4 (2016)
Downloads
Download data is not yet available.
+
−