{"id":117800,"date":"2015-06-07T00:00:00","date_gmt":"2015-06-07T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/sobre-la-equivalencia-entre-semanticas-operacionales-y-denotacionales-para-lenguajes-funcionales-paralelos\/"},"modified":"2015-06-07T00:00:00","modified_gmt":"2015-06-07T00:00:00","slug":"sobre-la-equivalencia-entre-semanticas-operacionales-y-denotacionales-para-lenguajes-funcionales-paralelos","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/complutense-de-madrid\/sobre-la-equivalencia-entre-semanticas-operacionales-y-denotacionales-para-lenguajes-funcionales-paralelos\/","title":{"rendered":"Sobre la equiValencia entre sem\u00e1nticas operacionales y denotacionales para lenguajes funcionales paralelos"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Lidia S\u00e1nchez Gil <\/strong><\/h2>\n<p>Eden es un lenguaje funcional paralelo que extiende haskell con construcciones sint\u00e1cticas para especificar la creaci\u00f3n de procesos. En eden se distinguen dos partes: un lambda c\u00e1lculo perezoso y expresiones de coordinaci\u00f3n. El lenguaje jauja es una simplificaci\u00f3n de eden que mantiene sus principales caracter\u00edsticas. El objetivo de esta tesis es dar los primeros pasos para demostrar la equiValencia entre las sem\u00e1nticas definidas para jauja por hidalgo-herrero. Se quiere probar la equiValencia en t\u00e9rminos de correcci\u00f3n y adecuaci\u00f3n computacional entre una sem\u00e1ntica operacional y una sem\u00e1ntica denotacional. Para hacerlo nos basamos en las ideas expuestas por launchbury, en el que se demuestra la equiValencia entre una sem\u00e1ntica natural y una sem\u00e1ntica denotacional est\u00e1ndar para un lambda c\u00e1lculo extendido con declaraciones locales.  puesto que demostrar la equiValencia entre las sem\u00e1nticas definidas para jauja supone un estudio demasiado complejo para afrontarlo en un primer paso, hemos comenzado por considerar una extensi\u00f3n del lenguaje utilizado por launchbury al que se ha a\u00f1adido una aplicaci\u00f3n paralela que da lugar a creaciones de procesos y comunicaciones entre ellos, es decir, a un sistema distribuido formado por distintos procesos que interact\u00faan entre s\u00ed. A partir de este sencillo lenguaje el estudio se desarrolla en varias etapas en las que se establece la equiValencia entre distintas sem\u00e1nticas operacionales y denotacionales para modelos distribuidos y no distribuidos. La sem\u00e1ntica operacional del modelo distribuido heredada de jauja es una sem\u00e1ntica de paso corto para varios procesadores. Para realizar la equiValencia de esta sem\u00e1ntica con una sem\u00e1ntica denotacional est\u00e1ndar extendida, con objeto de dotar de significado a la aplicaci\u00f3n paralela, se introducen dos sem\u00e1nticas intermedias: una de paso corto pero limitada a un \u00fanico procesador y una sem\u00e1ntica de paso largo que es una extensi\u00f3n de la sem\u00e1ntica natural de launchbury. En el caso de prescindir de las aplicaciones paralelas, la sem\u00e1ntica natural de launchbury y nuestra extensi\u00f3n se comportan igual.  con respecto al modelo no distribuido, y con el fin de completar las demostraciones ausentes en el trabajo de launchbury, se construye un espacio de funciones para los valores de la sem\u00e1ntica denotacional con recursos introducida por el autor. Posteriormente, se comprueba que es equivalente a la sem\u00e1ntica denotacional est\u00e1ndar bajo la condici\u00f3n de disponer de infinitos recursos. Tambi\u00e9n se estudian algunas relaciones existentes entre heaps y pares (heap, t\u00e9rmino) que se aplican para estudiar la equiValencia de las dos sem\u00e1nticas operacionales introducidas por launchbury.  hemos realizado gran parte del estudio utilizando la notaci\u00f3n localmente sin nombres, situada a medio camino entre la de nombres y la de de bruijn. As\u00ed se evitan  los problemas derivados de la notaci\u00f3n con nombres, es decir, tener que trabajar con t\u00e9rminos alfa equivalentes. Por otra parte, tambi\u00e9n se eluden las desventajas de utilizar solo los \u00edndices de de bruijn, que resultan complicados de manejar y dificultan la lectura de los t\u00e9rminos.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Sobre la equiValencia entre sem\u00e1nticas operacionales y denotacionales para lenguajes funcionales paralelos<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Sobre la equiValencia entre sem\u00e1nticas operacionales y denotacionales para lenguajes funcionales paralelos <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Lidia S\u00e1nchez Gil <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Complutense de Madrid<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 06\/07\/2015<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Yolanda Ortega Mallen<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: david de Frutos escrig <\/li>\n<li>arthur Chargueraud (vocal)<\/li>\n<li>phil Trinder (vocal)<\/li>\n<li>Santiago Escobar rom\u00e1n (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Lidia S\u00e1nchez Gil Eden es un lenguaje funcional paralelo que extiende haskell con construcciones sint\u00e1cticas para especificar [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[986,13880,6474,6473],"tags":[231932,195947,231931,231933,76937,30776],"class_list":["post-117800","post","type-post","status-publish","format-standard","hentry","category-complutense-de-madrid","category-informatica","category-lenguajes-de-programacion","category-teoria-de-la-programacion","tag-arthur-chargueraud","tag-david-de-frutos-escrig","tag-lidia-sanchez-gil","tag-phil-trinder","tag-santiago-escobar-roman","tag-yolanda-ortega-mallen"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/117800","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=117800"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/117800\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=117800"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=117800"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=117800"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}