Synonymous variables interleaved when using polymorphic functions

[nigelflower]

created by aualsop on Aug 18, 2019

In the tree below, node1 is a polymorphic function with two different λp terms. The bracketing should make the expression unambiguous, but it is misinterpreted after combining with node2. There is a λp'_t where there should be a λp_t:

***expected: λpʹ_t.∃x_tt.[x = [λp_t.[p_t = is-raining]]] ∧ [p'_t = [ask(john,x)]]

This issue does not arise when node1 is replaced with similar node3, which is of fixed type:

[nigelflower]

aualsop commented on Aug 19, 2019

Bug can be reproduced with the code below:

Bug: variables interleaved

# Global declarations

multiple letter identifiers

use rule function application
use rule non-branching nodes
use rule predicate modification
use rule lambda abstraction

# Constants and variables

constants of type e: john mary
variables of type 'a: x y z
variables of type tt: P
constants of type t: is-raining

###############################################################
# Lexicon

define John, john: john

define ask, asks, asked: LP.Lx_e.ask(x,P)

define node1: Lf_<tt,'bt>.Lp_'b.Ex_<t,t>.[x = Lp_t.[p = is-raining]] & f(x)(p)

define node3: Lf_<tt,tt>.Lp_t.Ex_<t,t>.[x = Lp_t.[p = is-raining]] & f(x)(p)

define node2: Lv1_<t,t>.Lx'_t.x' = ask(john,v1)

#################################################################

# Figures

exercise tree
title Bug: lambda variables are interleaved

# BUG HERE
# EXPECTED: λpʹ_t.∃x.[x = [λp_t.p_t = is-raining]] ∧ [p'_t = [ask(john,x)]]
# ACTUAL:   λp'_t.∃x.[x = [λp_t.p'_t = is-raining]] ∧ [p'_t = [ask(john,x)]]
instructions Bug: p and p' are interleaved, resulting in incorrect root node. Node 1 is a polymorphic function.
[ node1 node2 ]

# NO BUG HERE
# EXPECTED AND ACTUAL: λpʹ.∃x.[x = [λp_t.p = is-raining]] ∧ [pʹ = ask(john,x)]
instructions When polymorphic node 1 is replaced with non-polymorphic node3, the derivation proceeds as expected. The binding configuration by the two p variables is conserved.
[ node3 node2 ]