{"action":"created","issue":{"url":"https://api.github.com/repos/spechub/Hets/issues/172","repository_url":"https://api.github.com/repos/spechub/Hets","labels_url":"https://api.github.com/repos/spechub/Hets/issues/172/labels{/name}","comments_url":"https://api.github.com/repos/spechub/Hets/issues/172/comments","events_url":"https://api.github.com/repos/spechub/Hets/issues/172/events","html_url":"https://github.com/spechub/Hets/issues/172","id":34982091,"number":172,"title":"signatures versus theories\n","user":{"login":"sternk","id":2765467,"avatar_url":"https://avatars.githubusercontent.com/u/2765467?v=3","gravatar_id":"","url":"https://api.github.com/users/sternk","html_url":"https://github.com/sternk","followers_url":"https://api.github.com/users/sternk/followers","following_url":"https://api.github.com/users/sternk/following{/other_user}","gists_url":"https://api.github.com/users/sternk/gists{/gist_id}","starred_url":"https://api.github.com/users/sternk/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sternk/subscriptions","organizations_url":"https://api.github.com/users/sternk/orgs","repos_url":"https://api.github.com/users/sternk/repos","events_url":"https://api.github.com/users/sternk/events{/privacy}","received_events_url":"https://api.github.com/users/sternk/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/spechub/Hets/labels/C:logic","name":"C:logic","color":"0000aa"},{"url":"https://api.github.com/repos/spechub/Hets/labels/P:critical","name":"P:critical","color":"ffffb8"},{"url":"https://api.github.com/repos/spechub/Hets/labels/T:feature","name":"T:feature","color":"cccccc"}],"state":"open","locked":false,"assignee":{"login":"mcodescu","id":1632930,"avatar_url":"https://avatars.githubusercontent.com/u/1632930?v=3","gravatar_id":"","url":"https://api.github.com/users/mcodescu","html_url":"https://github.com/mcodescu","followers_url":"https://api.github.com/users/mcodescu/followers","following_url":"https://api.github.com/users/mcodescu/following{/other_user}","gists_url":"https://api.github.com/users/mcodescu/gists{/gist_id}","starred_url":"https://api.github.com/users/mcodescu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mcodescu/subscriptions","organizations_url":"https://api.github.com/users/mcodescu/orgs","repos_url":"https://api.github.com/users/mcodescu/repos","events_url":"https://api.github.com/users/mcodescu/events{/privacy}","received_events_url":"https://api.github.com/users/mcodescu/received_events","type":"User","site_admin":false},"assignees":[{"login":"mcodescu","id":1632930,"avatar_url":"https://avatars.githubusercontent.com/u/1632930?v=3","gravatar_id":"","url":"https://api.github.com/users/mcodescu","html_url":"https://github.com/mcodescu","followers_url":"https://api.github.com/users/mcodescu/followers","following_url":"https://api.github.com/users/mcodescu/following{/other_user}","gists_url":"https://api.github.com/users/mcodescu/gists{/gist_id}","starred_url":"https://api.github.com/users/mcodescu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mcodescu/subscriptions","organizations_url":"https://api.github.com/users/mcodescu/orgs","repos_url":"https://api.github.com/users/mcodescu/repos","events_url":"https://api.github.com/users/mcodescu/events{/privacy}","received_events_url":"https://api.github.com/users/mcodescu/received_events","type":"User","site_admin":false}],"milestone":null,"comments":4,"created_at":"2014-06-04T17:28:13Z","updated_at":"2016-08-03T05:43:02Z","closed_at":null,"body":"Reported by **till** and assigned to **mcodescu**\n Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/172\n\n\n***\n\nImplement a clean treatment of signatures versus theories. (Currently, often signatures also store some theory information. Some comorphisms are non-simple theoroidal, which is currently not backed by the general theory of heterogeneous specs.)\nsome notions:\n  * a simple theoroidal comorphism maps\n      * signatures to theories\n      * sentences to sentences\n      * the mapping of theories is induced by these maps\n  * an arbitrary theoroidal comorphism maps\n      * theories to theories\n      * sentences to sentences\n      * problem here: is doable, but more complicated than the simple case. do we really need it?\n  * a specification frame morphism maps\n      * theories to theories\n      * problem here: how to translate goals? Perhaps extend the notion of theory such that some formulas are marked as goals\ngeneral questions:\n  * can we stay with simple theoroidal comorphisms, or do we need non-simple ones?\n  * does it help to add the institution of presentations for each institution in the logic graph?\n  * can we stay with sentence-to-sentence translation, or do we need something else?\nproblems with simple theoroidal comorphisms:\n  * CASL to Isabelle: free types are axioms in CASL, sig elements in Isabelle\n      * solution 1  \n          * free types are signature elements in CASL\n          * two-level construction of CASL:\n          * plain CASL sigs as in `RefMan`\n          * CASL sig = plain CASL theory = plain CASL sig + set of sort gen axioms\n          * CASL theory = CASL sig + set of axioms\n      * solution 2\n          * free types are axioms in Isabelle\n      * solution 3\n          * non-simple theoroidal comorphisms\n  * CASL to HasCASL\n      * In HasCASL, datatypes must be parts of the signature (needed for analysis of program blocks)\n      * If CASL adopts the same solution, we get a simple theoroidal comorphism\n      * If CASL does not so, we get a non-simple theoroidal comorphism\n  * HasCASL to Haskell\n      * no problem, since constructors are already determined by signature and program blocks lead to complete definition of a function\n  * CASLtoTopSort: needs derived sig mors\n    ```\n    s<t  included in s<t<u is mapped to\n    sort t; pred s:t  \"included in\"  sort u; preds s,t:u\n\n    ```\n      *   This \"included\" is only a derived signature morphism. It would be nice to have an institution independent notion of derived signature morphism here\n  * CASLtoSPASS:\n      * sort gen axioms need to become signature parts. They cannot be translated to axioms!  =&gt; semi-comorphism.  Better would be a kind of partial comorphism (after all, some sentences *can* be translated)\n  * CASL2SubCFOL\n      * some sorts get bottom elements. These sorts are computed from the signature and the sentences (i.e. type cast) when mapping the whole theory. Therefore mapping the signature and sentences separately may not work for all sentences\nAre there problems with theoroidal comorphisms (i.e. sentence to sentence translation)?\nSee also ticket #171.\nDiscuss implications for Hets and its connection to provers.\n"},"comment":{"url":"https://api.github.com/repos/spechub/Hets/issues/comments/237146535","html_url":"https://github.com/spechub/Hets/issues/172#issuecomment-237146535","issue_url":"https://api.github.com/repos/spechub/Hets/issues/172","id":237146535,"user":{"login":"mcodescu","id":1632930,"avatar_url":"https://avatars.githubusercontent.com/u/1632930?v=3","gravatar_id":"","url":"https://api.github.com/users/mcodescu","html_url":"https://github.com/mcodescu","followers_url":"https://api.github.com/users/mcodescu/followers","following_url":"https://api.github.com/users/mcodescu/following{/other_user}","gists_url":"https://api.github.com/users/mcodescu/gists{/gist_id}","starred_url":"https://api.github.com/users/mcodescu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mcodescu/subscriptions","organizations_url":"https://api.github.com/users/mcodescu/orgs","repos_url":"https://api.github.com/users/mcodescu/repos","events_url":"https://api.github.com/users/mcodescu/events{/privacy}","received_events_url":"https://api.github.com/users/mcodescu/received_events","type":"User","site_admin":false},"created_at":"2016-08-03T05:43:01Z","updated_at":"2016-08-03T05:43:01Z","body":"If not all OWL theory morphisms can be mapped along OWL22CASL(with datatypes added by-need), then we need to identify the sublogic of OWL that is the source sublogic of this comorphism - otherwise we don't have a comorphism."}}
{"actor":{"display_login":"mcodescu"}}