Meeting 7 Nov

[noughtmare]

TODO:

• Rewrite intro to say that the problem is to verify parsing implementation and conal has made a start, we extend that.

• Write outline of things I'm working on in the paper. Tighter feedback loop.

• Meet with Benedikt

  • Are we defining multifunctors?
  • What properties can we claim. What structures do we have if we add fixed points to Conal's definitions?

• Finish nullability work and if possible derivatives.

• Examples or phenomena

  • General statements without formal definitions yet
  • Also an example grammar with nested fix

• Think about the category, is it a functor category [String, Set]? What is String?

Alternative view: Language is an abstract syntax class equipped with an equivalence relation.

[noughtmare]

Here’s an example of a grammar where you need to nest fix (which I discussed with Benedikt after you left Casper):

-- X ::= X '+' X | Y
-- Y ::= Y '*' Y | '(' X ')' | 'x'
--
-- expr2 = fix (λ X → (X ⋆ '+' ⋆ X)
--                  ∪ fix (λ Y → Y ⋆ '*' ⋆ Y
--                             ∪ '(' ⋆ X ⋆ ')'
--                             ∪ 'x'))
--
expr2 : Desc 0
expr2 =
  fix ((var Fin.zero ⋆ ‵ ‵+ ⋆ var Fin.zero)
      ∪ fix (var Fin.zero ⋆ ‵ ‵* ⋆ var Fin.zero
           ∪ ‵ ‵[ ⋆ var (Fin.suc Fin.zero) ⋆ ‵ ‵]
           ∪ ‵ ‵x))

[noughtmare]

@benediktahrens I don't think the alternative representation of languages as abstract syntax with equivalence relations works, because two different strings may have the same abstract syntax. For example "1+2" and "1 + 2" (with spaces).

[benediktahrens]

@noughtmare : I had not thought of that. But I disagree with your conclusion. Instead, I would say that the equivalence relation on strings is not the trivial one (as we said in our discussion), but instead one that throws away meaningless characters (like the spaces).

More generally, I would not say that a mathematical model "works" or "does not work". It might capture, or not, certain phenomena. If it does not capture a given phenomenon that we want it to capture, then it needs to be refined. ("Refinement" usually means that it needs to be made more complicated.) This is an iterative process, in my experience.

Here, this could mean that instead of considering one morphism of setoids, it could be useful to consider a commutative triangle of setoids, or some such thing - that's the research part!