Artículos con la etiqueta ‘cálculo lambda’

Logical systems II: Free semantics

Por • 15 ene, 2014 • Category: Crítica

This paper is a sequel to “Logical systems I: Lambda calculi through discreteness”. It provides a general 2-categorical setting for extensional calculi and shows how intensional and extensional calculi can be related in logical systems. We focus on transporting the notion of Day convolution to a 2-categorical framework, and as a complementary result we prove the convolution theorem for internal categories. We define the concept of Yoneda triangle, and show how objects in a Yoneda bitriangle get extensional semantics “for free”. This includes the usual semantics for propositional calculi, Kripke semantics for intuitionistic calculi and ternary frame semantics for substructural calculi including Lambek’s lambda calculi, relevance and linear logics. We show how in this setting, one may use a model-theoretic logic to induce a structure of a proof-theoretic logic.

Extensionality of lambda-*

Por • 7 ene, 2014 • Category: Opinion

We prove an extensionality theorem for the “type-in-type” dependent type theory with Sigma-types. We suggest that the extensional equality type be identified with the logical equivalence relation on the free term model of type theory.

GLC actors, artificial chemical connectomes, topological issues and knots

Por • 25 dic, 2013 • Category: Educacion

Based on graphic lambda calculus, we propose a program for a new model of asynchronous distributed computing, inspired from Hewitt Actor Model, as well as several investigation paths, concerning how one may graft lambda calculus and knot diagrammatics.