# Tag Info

9

A major idea of concatenative languages is that the syntax and semantic domain form monoids and the semantics is a monoid homomorphism. The syntax is the free monoid generated by the basic operations, better known as a list. It's operation is list concatenation, i.e. (++) in Haskell. In the untyped context, the semantic domain is just the monoid of ...

1

In the field of Denotational semantics they have developed a (very) formal definition of iteration in terms of recursive functions that you might like to look into. https://en.wikipedia.org/wiki/Denotational_semantics

1

The $k$th iteration is just the $k$th element of some appropriate sequence. In general, I doubt it's a formally defined concept; it's just one of those things whose meaning is basically the natural-language meaning of the word.

1

The assignment axiom in standard Hoare logic says: |- {P[e/x]}x:=e{P} If you choose P[e/x] to be x+1=44 (that is e is x+1) you get: |- {x+1=44} x:=x+1 {x=44} By the consequence rule, since: |= x=43 --> x+1=44, and |= x+1=44 --> x+1=44, and |- {x+1=44} x:=x+1 {x=44} you know that |- {x=43} x:=x+1 {x=44} . Since the Hoare logic is relatively complete ...

Only top voted, non community-wiki answers of a minimum length are eligible