Bug in 'put_tree -compute', and structural transfer in GF

[Hans Leiss]

Hi Aarne, Krasimir e.a.,

on p.3 on my slides to the GF-seminar on Jan.9th (attached as
slides-transfer.pdf), I mentioned that there was a bug in the
'put_tree -compute' of the gf-shell. In the meantime, I checked the
compiler code and found the mistake. The computation doesn't compare
patterns with non-data-declared fun's properly; on mismatch, the
search is stopped instead of using further def-equations. The bug and
its fix is explained in detail in point 4 of the attached
gf-bugs.ps. The fix itself is

diff --git a/src/runtime/haskell/PGF/Expr.hs b/src/runtime/haskell/PGF/Expr.hs
index ff1114235..bdc8e5e90 100644
--- a/src/runtime/haskell/PGF/Expr.hs
+++ b/src/runtime/haskell/PGF/Expr.hs
@@ -408,7 +408,8 @@ match sig f eqs as0 =
tryMatch (p ) (VMeta i envi vs ) env = VSusp i envi vs (\v -> tryMatch p v env)
tryMatch (p ) (VGen i vs ) env = VConst f as0
tryMatch (p ) (VSusp i envi vs k) env = VSusp i envi vs (\v -> tryMatch p (k v) env)
- tryMatch (p ) v@(VConst _ _ ) env = VConst f as0
+-- tryMatch (p ) v@(VConst _ _ ) env = VConst f as0
+ tryMatch (p ) v@(VConst _ _ ) env = match sig f eqs as0 -- HL 10.2.2025
tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env
tryMatch (PImplArg p ) (VImplArg v ) env = tryMatch p v env

I used flags 'pt -normalize=f tree' and 'pt -transfer=f tree' on the
slides, but after fixing the bug in Expr.hs, I had to change the
definition of 'normalize'. Subsequently I also renamed the flags to

'pt -transfer=f tree' and 'pt -apply=f tree'

so that, in case the 'transfer' flag should be made available in
gf-3.12, the example of 'pt -transfer=iS' on p.195 of the GF-book
would work again.

I havn't yet made a git-branch of the material on DLang and the
transfer examples I showed on the slides (because I accidentally
started doing this on another, unsynchronized git-branch), but an
extensive description is attached as gf-structural-transfer.ps

Hans


Akademischer Direktor am CIS bis März 2017 (seitdem im Ruhestand)
-------------------------------------------------------------------------
Dr.Hans Leiß le...@cis.uni-muenchen.de
Centrum für Informations- www.cis.uni-muenchen.de/~leiss/
und Sprachverarbeitung (CIS)
Universität München
Oettingenstr. 67
D-80538 München
-------------------------------------------------------------------------

[Aarne Ranta]

Hi Hans,

Thanks for all the comments and the fix proposal! I cannot see it as a pull request yet. There are some pull requests waiting (sorry, community), but I think this is quite independent of them and could be dealt with separately. At least it is one that I might dare to look at myself, unlike many others. Re-enabling transfer is certainly a welcome feature, even though the old way to do it is not the most practical one (compared to what I think Krasimir is preparing).

Your talk revived some ideas, also in connection working on Dedukti, which is a minimalistic LF very similar to GF's abstract syntax (and the old ALF). The way constructors and functions are treated in Dedukti is very much what I had in mind (under the influence of ALF), and I wonder whether not to make sure that we do it the same way again. This would probably fix some of your issues, but contradict some explanations in the GF book. However, the book was promised to be compatible with just GF 3.2. Later changes should, nevertheless, in my opinion, not break any old code written in the GF language. But later changes can make new things possible - such as dividing data types and function cases to different tiles.

The GF shell is not included in the 3.2 commitment, but I think reasonable functionalities should always be kept if possible.

In Dedukti,

- you can split constructors for a type into different files

- you can split rewrite rules (corresponding to GF's def rules) for the same function in different files

- declarations of constructor funs (GF's data) are distinct from declarations of defined functions (GF's fun)

see https://github.com/Deducteam/Dedukti/blob/master/README.md 

The reason why splitting data and def rules in ALF was allowed was that def rules were not allowed to be overlapping. This was not checked by the system, as far as I remember, but it prevents the problem that Krasimir mentioned, namely how to order the def rules. If they don't overlap, then their order does not matter. In Dedukti, there is a slightly weaker condition: the rewrite rules should be confluent, that is, yield the same results independently of their order of application. Confluence is not checked by default, but there is a flag that forces a check.

Splitting constructors and defs was - and is - very useful in grammars that have a rule-by-rule semantics. A grammar with a large lexicon can have lexical entries in different modules, introduced and given semantics at the same time:

  - fun semanticsN : N -> Set

  - data bachelor_N : N ;

  - def semanticsN bachelor_N = Sigma man unmarried

In fact, the linearization rules of GF have always worked in this way: if you see lin as a function defined by pattern matching, its definition is clearly split into different tiles. Before GF, when I wrote grammars in ALF, I would have written (the equivalent of)

  - data bachelor_N : N ;

  - def semanticsN bachelor_N = Sigma man unmarried

  - def linN backelor_N = mkN "bachelor"

This makes it clear that linearization is a kind of rule-by-rule (compositional) semantics - with an even stronger condition than non-overlap, because you cannot use variables for data constructors or separate different cases for their arguments.

Sorry if I have made a short story long or interpreted your suggestions incorrectly. My summary of an action plan is: 

- re-enable pt -transfer

- re-enable splitting constructors and def rules into files (with a note on expected confluence)

- maintain the data/fun distinction? seems safest to me, but I would then like to convert all RGL funs into data functions

Regards

  Aarne

--

---
You received this message because you are subscribed to the Google Groups "Grammatical Framework" group.
To unsubscribe from this group and stop receiving emails from it, send an email to gf-dev+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/gf-dev/20250212150411.137EE7E1C1D%40marmolata.cis.uni-muenchen.de.

[Hans Leiss]

Hi Aarne,

sorry for not making a pull request yet. I wanted to add an explanation
of the bug, to give you a better chance to check the correction of the
fix. Also, I wasn't sure whether you really want to add the transfer
flag again, in particular since I don't know exactly what Krasimir is
preparing. What I wanted to say is

1. the current pt -compute has a little bug, and how to fix it.
2. without the possibility to pipe a parse tree to pt -compute, the
-compute flag is rather useless, so better provide -transfer again.
3. I believe there are application-independent uses of structural
transfer, so tree transfer should be/remain part of GF.
4. it may be worth thinking of fun's with def-rules in concrete instead
of abstract grammars, to enable translation by piping parse trees to
target-specific (linearization o transfer) (Remark 120 on gf-bugs.pdf).

I can prepare a pull request, but maybe little changes in the shell
help+examples are needed. On the slides for the GF-seminar, I
distinguished 'pt -normalize=f tree' for functions f : C -> C from 'pt
-transfer=g tree' for functions g : C -> D', where I had in mind
syntax-tree transformations f replacing (maximal) subtrees of type C by
their values under f. If the more general tranfers g were used this way,
they would create type-incorrect trees. Renaming -normalize to -transfer
is ok (if the help comment removes the restriction to 'type-preserving'
f), since the code doesn't check that input and output type of f agree.
[I forgot that the transfer functions like iS : S -> Prop in the GF-book
is not 'type-preserving'.] Then also, a separate flag -apply for the
transfers g could be dropped.

Thanks for your comments about Dedukti, ALF etc. Yes, I also see lin as
a function defined by pattern matching split over different tiles. GF
only demands that all fun/data f : A -> B with the same B are in the
same module, e.g. all CN-constructors in the module Noun -- but GF does
not demand that this is the same module where B is defined (which is
Cat, not Noun), contradicting C.3.6 of the book (cf. 3. in gf-bugs.pdf).

Indicated in 4. above, all transfers g : B -> C with the same B could
also be in this module, since patterns over B are available there.
However, for the tree normalizations I have in mind, I share Krasimir's
doubts on order-independence of def-rules; my def-rules for nfCN : CN >
CN certainly are order-dependent (as is the use of equations in 'pt
-compute').

It is unclear to me how the target-language specific tree transfer
functions indicated under 4. and the target-language independent
computation rules for semantics should be related.

Regards,

Hans

[Aarne Ranta]

Hello Hans,

It is clear that bug fixes are welcome, and they are better treated via pull requests - so that a full credit is given to their authors.

I also think the transfer flag should be restored. It does not make any harm anywhere else.

However, I am not sure how far we can get with transfer rules defined in the current set-up with GF's def-definitions. I would like to get back to the old set-up where def rules and data functions can be split to different modules (like in ALF and Dedukti). I am not insisting on this, because I don't have time to carry it out with all the consequences it has (and don't expect anyone else to have). BUT, if it is done, it will make it impossible to have catch-all cases with wildcards, because they would easily leave to non-confluent definitions when clauses from different modules are combined.

Transfer in concrete syntax? I agree that the desired translations are often language-specific. But I would still rather define them in one place and let each language in a multilingual system to decide which transfers to use. This must at the moment be done in a host language (like all transfer anyway in the absence of -transted flag)

---------- a bit beside the point, but as a perspective on transfer:

Actually I am working a lot on transfer right now in the Informath project. The way I do it in Haskell is crucially based on the the PGF view, where all modules are combined into one datatype in Haskell - actually a GADT, where all GF categories are instances of a universal (Tree a) type. In the current version, e.g. the module 

https://github.com/aarneranta/gf-math/blob/main/v3/Core2Informath.hs

generates variants of a given MathCore statement with a sequence of transfer functions, each doing "just one thing" in a way similar to compiler optimizations. For example, 

- the function "aggregate" turns "x is even or x is odd" to "x is even or odd"

- the function "formalize" turns "the sum of x and y" to "x and y"

Two aspects of this are outside the reach of GF's def definitions:

- catch-all cases using composOp (to avoid boilerplate code that just compositionally distributes the function to subtrees without doing anything else). This means that each function definition is just a few lines long, because it is "almost compositional"

- returning lists of variant trees; this is possible in GF, but very tedious in the absence of built-in list facilities

Notice that in the Haskell data type generation all GF functions are treated as constructors. I think this is as it should be: transfer is performed on syntax trees and not on their semantic values. This reminds me that, originally, GF's def rules were primarily meant to define the equality of dependent types, which is needed in type checking.

What about grammar extensions? The wishful idea is that such extensions are mainly done in the lexicon, i.e. fun functions of ground types (not function types). They can be treated uniformly in the GF to Haskell generation, by constructor applications such as (LexKind "set_Kind"). This means that Haskell transfer modules such as Core2Informath don't need to be modified. What is more, because of the automatically generated composOp functions, there is no need to modify the transfer modules even if non-lexical functions are added, as long as they behave compositionally in the "almost compositional" transfer operations.

Regards

  Aarne

--

---
You received this message because you are subscribed to the Google Groups "Grammatical Framework" group.
To unsubscribe from this group and stop receiving emails from it, send an email to gf-dev+un...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/gf-dev/crbv7tcs6r9.fsf%40mailhost.cis.uni-muenchen.de.

[Hans Leiss]

Hello Aarne,

> It is clear that bug fixes are welcome, and they are better treated via pull requests - so that a full credit is
> given to their authors.

I had made a pull request #174 to gf-core (before I went off for travelling), some checks succeeded, some failed.

> I also think the transfer flag should be restored. It does not make any harm anywhere else.
>
> However, I am not sure how far we can get with transfer rules defined in the current set-up with GF's
> def-definitions. I would like to get back to the old set-up where def rules and data functions can be split to
> different modules (like in ALF and Dedukti).

It is clear that the def-rules of GF only give a limited class of transfer functions, but it is/was something.
A separation of data f:A -> C into fun f:A -> C and data C = f will not work for GF, as long as all
constructor definitions data C = f must appear in the module where C is defined (as C.3.6 says): this module
is Cat, which does not know which functions f will be declared in other modules (M = Cat ** {fun f : A -> C; ...}).

> I am not insisting on this, because I don't have time to carry it
> out with all the consequences it has (and don't expect anyone else to have). BUT, if it is done, it will make it
> impossible to have catch-all cases with wildcards, because they would easily leave to non-confluent definitions
> when clauses from different modules are combined.
>
> Transfer in concrete syntax? I agree that the desired translations are often language-specific. But I would still
> rather define them in one place and let each language in a multilingual system to decide which transfers to use.
> This must at the moment be done in a host language (like all transfer anyway in the absence of -transted flag)
>

It could perhaps be done in one place if the def-rules of transfer functions f : A -> C (implicitly) had a language
parameter, def f L1 pat = term1 | f L2 pat = term2 | ..., and linearization o transfer used this parameter as
a flag -lang=Li.

Sounds good, but I'm not sure if I fully understand this. (At least, transfer is partly motivated by the wish
to bypass compositionality.)

But I have a general question about grammar extensions: Some fun's are declared both in Extra.gf and
Extend.gf. I would like to clean up this for Ger by removing declarations from ExtraGerAbs if they are also in
Extend, so that I can reserve ExtraGerAbs for constructions special for Ger (e.g. rules with correlates for
sentential or infinitival objects) and have ExtraGer and ExtendGer distinct. Would such a change of ExtraGer
break the backward compatibility?

Hans

[Inari]

Hi Hans, Aarne,

The errors in the CI have now been fixed (thanks Anka and Arianna!), so we are able to test your PR properly. 

There is a change of behavior in 3 test cases, see these lines:

https://github.com/GrammaticalFramework/gf-core/blob/master/testsuite/runtime/eval/Test.gf#L22-L24 

The test cases are different for the following:

pt -compute dec (succF zeroF)                -- expected: dec (succF zeroF),  got: err

pt -compute dec zeroF                        -- expected: dec zeroF,  got: err

pt -compute <\x -> dec (dec x) : Nat -> Nat> -- expected: \v0 -> dec (dec v0), got: \v0 -> err

I don't know what any of this means. Maybe we can look at it at the summer school.

Inari