It should be noticed that interpretation of types is very different from
the interpretation of terms. The connection between the two is the soundness
theorem: the interpretation of term is in the interpretation of types.
Thursday, July 29, 2010
Thursday, July 15, 2010
New thoughts on 7/15
I just realize that the applicative structure is just not expressive enough to
describe the axioms. I need a more expressive signature.
describe the axioms. I need a more expressive signature.
Learning note 7/15
1. Term algebra provides us an algebraic formalization on the term signature, so that
we can use tool from algebra to study term. So in a sense, Herbrand is a smart guy.
2. The only identities or equational classes in term algebra are those syntatical identities.
3. It is(is it?) possible to have a sigma-algebras which has it's own equational classes that can not be formalized by the identities in sigma-signature.
4. A spec=<\sigma,E> is only a form of algebraic specification, we can replace E by
a bunch of axioms.
we can use tool from algebra to study term. So in a sense, Herbrand is a smart guy.
2. The only identities or equational classes in term algebra are those syntatical identities.
3. It is(is it?) possible to have a sigma-algebras which has it's own equational classes that can not be formalized by the identities in sigma-signature.
4. A spec=<\sigma,E> is only a form of algebraic specification, we can replace E by
a bunch of axioms.
Subscribe to:
Posts (Atom)